blob: fd80cec6f589d27d0c1af05f62faabc0c641c333 (
plain)
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
33
34
|
(* 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.
(* Check that no tuple needs to be built *)
Lemma l3 : (x,y:nat)
(existS ? [n:nat]({n=n}+{n=n}) x (left ? ? (refl_equal nat x)))=
(existS ? [n:nat]({n=n}+{n=n}) y (left ? ? (refl_equal nat y)))
-> x=y.
Intros x y H.
Injection H.
Exact [H]H.
Qed.
(* Check that a tuple is built (actually the same as the initial one) *)
Lemma l4 : (p1,p2:{O=O}+{O=O})
(existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2)
->(existS ? [n:nat]({n=n}+{n=n}) O p1)=(existS ? [n:nat]({n=n}+{n=n}) O p2).
Intros.
Injection H.
Exact [H]H.
Qed.
|
