1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
|
Goal forall x, x = 0 -> S x = 7 -> x = 22 .
Proof.
replace 0 with 33.
Undo.
intros x H H0.
replace x with 0.
Undo.
replace x with 0 in |- *.
Undo.
replace x with 1 in *.
Undo.
replace x with 0 in *|- *.
Undo.
replace x with 0 in *|-.
Undo.
replace x with 0 in H0 .
Undo.
replace x with 0 in H0 |- * .
Undo.
replace x with 0 in H,H0 |- * .
Undo.
Admitted.
(* This failed at some point when "replace" started to support arguments
with evars but "abstract" did not supported any evars even defined ones *)
Class U.
Lemma l (u : U) (f : U -> nat) (H : 0 = f u) : f u = 0.
replace (f _) with 0 by abstract apply H.
reflexivity.
Qed.
|
