blob: 34338662398851996bb79baaf408e96ffc6d9a93 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
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.
Goal 1 = 0 -> 0 = 1.
intro H.
Fail rewrite H at 1 2 3. (* bug #13566 *)
Fail rewrite H at 0.
rewrite H at 1.
reflexivity.
Qed.
|
