1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 set "baseuri" "cic:/matita/test/prova".
17 include "LAMBDA-TYPES/LambdaDelta-1/preamble.ma".
18 alias id "ty3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3.ind#xpointer(1/1)".
19 alias id "pc3" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/defs/pc3.con".
20 alias id "THead" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1/3)".
21 alias id "T" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/T.ind#xpointer(1/1)".
22 alias id "G" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/G/defs/G.ind#xpointer(1/1)".
23 alias id "Flat" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1/2)".
24 alias id "Cast" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1/2)".
25 alias id "C" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/C/defs/C.ind#xpointer(1/1)".
32 .ty3 g c (THead (Flat Cast) t2 t1) x
33 \rarr pc3 c t2 x\land ty3 g c t1 t2)
36 intros 6 (g c t1 t2 x H).
37 apply insert_eq;(* 6 P P P C I I 3 0 *)
38 [apply T(* dependent *)
39 |apply (THead (Flat Cast) t2 t1)(* dependent *)
40 |apply (\lambda t:T.ty3 g c t x)(* dependent *)
42 alias id "ty3_ind" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/defs/ty3_ind.con".
43 elim H0 using ty3_ind names 0;(* 13 P C I I I I I I I C C C I 12 3 *)
44 [intros 11 (c0 t0 t UNUSED UNUSED u t3 UNUSED H4 H5 H6).
45 letin H7 \def (f_equal T T (\lambda e:T.e) u (THead (Flat Cast) t2 t1) H6).(* 6 C C C C C I *)
47 rewrite > H7 in H4:(%) as (H8).
48 cut (pc3 c0 t2 t3\land ty3 g c0 t1 t2) as H10;
51 apply refl_equal(* 2 C C *)
53 elim H10 using and_ind names 0.(* 5 P P C I I 3 0 *)
55 apply conj;(* 4 C C I I *)
56 [alias id "pc3_t" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_t.con".
57 apply pc3_t;(* 6 P C C I C I *)
58 [apply t3(* dependent *)
59 |apply H11(* assumption *)
60 |apply H5(* assumption *)
62 |apply H12(* assumption *)
65 alias id "K" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/K.ind#xpointer(1/1)".
66 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
67 [TSort (_:nat)\rArr True
68 |TLRef (_:nat)\rArr False
69 |THead (_:K) (_:T) (_:T)\rArr False] as H2;
71 |rewrite < H1 in \vdash (%).
75 change in H2:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
76 [TSort (_:nat)\rArr True
77 |TLRef (_:nat)\rArr False
78 |THead (_:K) (_:T) (_:T)\rArr False].
79 elim H2 using False_ind names 0(* 2 C I 2 0 *)
80 |intros 9 (n c0 d u UNUSED t UNUSED UNUSED H4).
81 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
82 [TSort (_:nat)\rArr False
83 |TLRef (_:nat)\rArr True
84 |THead (_:K) (_:T) (_:T)\rArr False] as H5;
86 |rewrite < H4 in \vdash (%).
90 change in H5:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
91 [TSort (_:nat)\rArr False
92 |TLRef (_:nat)\rArr True
93 |THead (_:K) (_:T) (_:T)\rArr False].
94 elim H5 using False_ind names 0(* 2 C I 2 0 *)
95 |intros 9 (n c0 d u UNUSED t UNUSED UNUSED H4).
96 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
97 [TSort (_:nat)\rArr False
98 |TLRef (_:nat)\rArr True
99 |THead (_:K) (_:T) (_:T)\rArr False] as H5;
101 |rewrite < H4 in \vdash (%).
105 change in H5:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
106 [TSort (_:nat)\rArr False
107 |TLRef (_:nat)\rArr True
108 |THead (_:K) (_:T) (_:T)\rArr False].
109 elim H5 using False_ind names 0(* 2 C I 2 0 *)
110 |intros 14 (c0 u t UNUSED UNUSED b t0 t3 UNUSED UNUSED t4 UNUSED UNUSED H7).
111 alias id "F" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/F.ind#xpointer(1/1)".
112 alias id "B" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/T/defs/B.ind#xpointer(1/1)".
113 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
114 [TSort (_:nat)\rArr False
115 |TLRef (_:nat)\rArr False
116 |THead (k:K) (_:T) (_:T)\rArr
117 match k in K return \lambda _:K.Prop with
118 [Bind (_:B)\rArr True|Flat (_:F)\rArr False]] as H8;
120 |rewrite < H7 in \vdash (%).
124 change in H8:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
125 [TSort (_:nat)\rArr False
126 |TLRef (_:nat)\rArr False
127 |THead (k:K) (_:T) (_:T)\rArr
128 match k in K return \lambda _:K.Prop with
129 [Bind (_:B)\rArr True|Flat (_:F)\rArr False]].
130 elim H8 using False_ind names 0(* 2 C I 2 0 *)
131 |intros 10 (c0 w u UNUSED UNUSED v t UNUSED UNUSED H5).
132 cut match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
133 [TSort (_:nat)\rArr False
134 |TLRef (_:nat)\rArr False
135 |THead (k:K) (_:T) (_:T)\rArr
136 match k in K return \lambda _:K.Prop with
137 [Bind (_:B)\rArr False
139 match f in F return \lambda _:F.Prop with
140 [Appl\rArr True|Cast\rArr False]]] as H6;
142 |rewrite < H5 in \vdash (%).
146 change in H6:(%) with match THead (Flat Cast) t2 t1 in T return \lambda _:T.Prop with
147 [TSort (_:nat)\rArr False
148 |TLRef (_:nat)\rArr False
149 |THead (k:K) (_:T) (_:T)\rArr
150 match k in K return \lambda _:K.Prop with
151 [Bind (_:B)\rArr False
153 match f in F return \lambda _:F.Prop with
154 [Appl\rArr True|Cast\rArr False]]].
155 elim H6 using False_ind names 0(* 2 C I 2 0 *)
156 |intros 9 (c0 t0 t3 H1 H2 t4 UNUSED UNUSED H5).
157 letin H6 \def (f_equal T T
159 .match e in T return \lambda _:T.T with
160 [TSort (_:nat)\rArr t3
161 |TLRef (_:nat)\rArr t3
162 |THead (_:K) (t:T) (_:T)\rArr t]) (THead (Flat Cast) t3 t0)
163 (THead (Flat Cast) t2 t1) H5).(* 6 C C C C C I *)
164 alias id "pc3_refl" = "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/pc3/props/pc3_refl.con".
165 letin DEFINED \def (let H7 \def
168 .match e in T return \lambda _:T.T with
169 [TSort (_:nat)\rArr t0
170 |TLRef (_:nat)\rArr t0
171 |THead (_:K) (_:T) (t:T)\rArr t])
172 (THead (Flat Cast) t3 t0) (THead (Flat Cast) t2 t1) H5
178 .t0=THead (Flat Cast) t2 t1
179 \rarr pc3 c0 t2 t\land ty3 g c0 t1 t2) H2 t2 H8
181 let H12 \def eq_ind T t3 (\lambda t:T.ty3 g c0 t0 t) H1 t2 H8 in
182 eq_ind_r T t2 (\lambda t:T.pc3 c0 t2 t\land ty3 g c0 t1 t2)
183 (let H14 \def eq_ind T t0 (\lambda t:T.ty3 g c0 t t2) H12 t1 H7 in
184 conj (pc3 c0 t2 t2) (ty3 g c0 t1 t2) (pc3_refl c0 t2) H14) t3
186 apply DEFINED.(* 1 I *)
187 apply H6(* assumption *)
189 |apply H(* assumption *)