test-suite/success/rewrite_in.v


1
2
3
4
5
6
7
8

Require Import Setoid.

Goal forall (P Q : Prop) (f:P->Prop) (p:P), (P<->Q) -> f p -> True.
  intros P Q f p H.
  rewrite H in p || trivial.
Qed.