blob: a0b564c7254778eb2978477ba480404c531528f7 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
Goal False.
Proof.
set (H1:=I).
set (x:=true).
assert (H2: x = true) by reflexivity.
set (y:=false).
assert (H3: y = false) by reflexivity.
clearbody H1 x y.
eenough (H4: _ = false).
vm_compute in H4.
(* H4 now has "x:=y" in the evar context. *)
2: exact H3.
match type of H4 with y = false => idtac end.
Abort.
|
