blob: aecb7e1f60326189fd32b84453dbea017d867f57 (
plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
|
(* Check the behaviour of Injection *)
(* Check that Injection tries Intro until *)
Lemma l1 : (x:nat)(S x)=(S (S x))->False.
Injection 1.
Apply n_Sn.
Qed.
Lemma l2 : (x:nat)(H:(S x)=(S (S x)))H==H->False.
Injection H.
Intros.
Apply (n_Sn x H0).
Qed.
|
