blob: 8169361c4b90a4078a08e7b1ed8addfb180a4af2 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
|
Goal forall x:nat, (forall x, x=0 -> True)->True.
intros; eapply H.
instantiate (1:=(fun y => _) (S x)).
simpl.
clear x. trivial.
Qed.
Goal forall y z, (forall x:nat, x=y -> True) -> y=z -> True.
intros; eapply H.
rename z into z'.
clear H0.
clear z'.
reflexivity.
Qed.
|
