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 (* This file was automatically generated: do not edit *********************)
17 set "baseuri" "cic:/matita/LAMBDA-TYPES/Level-1/LambdaDelta/sn3/props".
27 include "iso/props.ma".
29 theorem sn3_pr3_trans:
30 \forall (c: C).(\forall (t1: T).((sn3 c t1) \to (\forall (t2: T).((pr3 c t1
31 t2) \to (sn3 c t2)))))
33 \lambda (c: C).(\lambda (t1: T).(\lambda (H: (sn3 c t1)).(sn3_ind c (\lambda
34 (t: T).(\forall (t2: T).((pr3 c t t2) \to (sn3 c t2)))) (\lambda (t2:
35 T).(\lambda (H0: ((\forall (t3: T).((((eq T t2 t3) \to (\forall (P:
36 Prop).P))) \to ((pr3 c t2 t3) \to (sn3 c t3)))))).(\lambda (H1: ((\forall
37 (t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P))) \to ((pr3 c t2 t3) \to
38 (\forall (t4: T).((pr3 c t3 t4) \to (sn3 c t4)))))))).(\lambda (t3:
39 T).(\lambda (H2: (pr3 c t2 t3)).(sn3_sing c t3 (\lambda (t0: T).(\lambda (H3:
40 (((eq T t3 t0) \to (\forall (P: Prop).P)))).(\lambda (H4: (pr3 c t3 t0)).(let
41 H_x \def (term_dec t2 t3) in (let H5 \def H_x in (or_ind (eq T t2 t3) ((eq T
42 t2 t3) \to (\forall (P: Prop).P)) (sn3 c t0) (\lambda (H6: (eq T t2 t3)).(let
43 H7 \def (eq_ind_r T t3 (\lambda (t: T).(pr3 c t t0)) H4 t2 H6) in (let H8
44 \def (eq_ind_r T t3 (\lambda (t: T).((eq T t t0) \to (\forall (P: Prop).P)))
45 H3 t2 H6) in (let H9 \def (eq_ind_r T t3 (\lambda (t: T).(pr3 c t2 t)) H2 t2
46 H6) in (H0 t0 H8 H7))))) (\lambda (H6: (((eq T t2 t3) \to (\forall (P:
47 Prop).P)))).(H1 t3 H6 H2 t0 H4)) H5)))))))))))) t1 H))).
49 theorem sn3_pr2_intro:
50 \forall (c: C).(\forall (t1: T).(((\forall (t2: T).((((eq T t1 t2) \to
51 (\forall (P: Prop).P))) \to ((pr2 c t1 t2) \to (sn3 c t2))))) \to (sn3 c t1)))
53 \lambda (c: C).(\lambda (t1: T).(\lambda (H: ((\forall (t2: T).((((eq T t1
54 t2) \to (\forall (P: Prop).P))) \to ((pr2 c t1 t2) \to (sn3 c
55 t2)))))).(sn3_sing c t1 (\lambda (t2: T).(\lambda (H0: (((eq T t1 t2) \to
56 (\forall (P: Prop).P)))).(\lambda (H1: (pr3 c t1 t2)).(let H2 \def H0 in
57 ((let H3 \def H in (pr3_ind c (\lambda (t: T).(\lambda (t0: T).(((\forall
58 (t3: T).((((eq T t t3) \to (\forall (P: Prop).P))) \to ((pr2 c t t3) \to (sn3
59 c t3))))) \to ((((eq T t t0) \to (\forall (P: Prop).P))) \to (sn3 c t0)))))
60 (\lambda (t: T).(\lambda (H4: ((\forall (t3: T).((((eq T t t3) \to (\forall
61 (P: Prop).P))) \to ((pr2 c t t3) \to (sn3 c t3)))))).(\lambda (H5: (((eq T t
62 t) \to (\forall (P: Prop).P)))).(H4 t H5 (pr2_free c t t (pr0_refl t))))))
63 (\lambda (t3: T).(\lambda (t4: T).(\lambda (H4: (pr2 c t4 t3)).(\lambda (t5:
64 T).(\lambda (H5: (pr3 c t3 t5)).(\lambda (H6: ((((\forall (t6: T).((((eq T t3
65 t6) \to (\forall (P: Prop).P))) \to ((pr2 c t3 t6) \to (sn3 c t6))))) \to
66 ((((eq T t3 t5) \to (\forall (P: Prop).P))) \to (sn3 c t5))))).(\lambda (H7:
67 ((\forall (t6: T).((((eq T t4 t6) \to (\forall (P: Prop).P))) \to ((pr2 c t4
68 t6) \to (sn3 c t6)))))).(\lambda (H8: (((eq T t4 t5) \to (\forall (P:
69 Prop).P)))).(let H_x \def (term_dec t4 t3) in (let H9 \def H_x in (or_ind (eq
70 T t4 t3) ((eq T t4 t3) \to (\forall (P: Prop).P)) (sn3 c t5) (\lambda (H10:
71 (eq T t4 t3)).(let H11 \def (eq_ind T t4 (\lambda (t: T).((eq T t t5) \to
72 (\forall (P: Prop).P))) H8 t3 H10) in (let H12 \def (eq_ind T t4 (\lambda (t:
73 T).(\forall (t6: T).((((eq T t t6) \to (\forall (P: Prop).P))) \to ((pr2 c t
74 t6) \to (sn3 c t6))))) H7 t3 H10) in (let H13 \def (eq_ind T t4 (\lambda (t:
75 T).(pr2 c t t3)) H4 t3 H10) in (H6 H12 H11))))) (\lambda (H10: (((eq T t4 t3)
76 \to (\forall (P: Prop).P)))).(sn3_pr3_trans c t3 (H7 t3 H10 H4) t5 H5))
77 H9))))))))))) t1 t2 H1 H3)) H2)))))))).
80 \forall (c: C).(\forall (u: T).((sn3 c u) \to (\forall (t: T).((sn3 c t) \to
81 (sn3 c (THead (Flat Cast) u t))))))
83 \lambda (c: C).(\lambda (u: T).(\lambda (H: (sn3 c u)).(sn3_ind c (\lambda
84 (t: T).(\forall (t0: T).((sn3 c t0) \to (sn3 c (THead (Flat Cast) t t0)))))
85 (\lambda (t1: T).(\lambda (_: ((\forall (t2: T).((((eq T t1 t2) \to (\forall
86 (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c t2)))))).(\lambda (H1: ((\forall
87 (t2: T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to
88 (\forall (t: T).((sn3 c t) \to (sn3 c (THead (Flat Cast) t2
89 t))))))))).(\lambda (t: T).(\lambda (H2: (sn3 c t)).(sn3_ind c (\lambda (t0:
90 T).(sn3 c (THead (Flat Cast) t1 t0))) (\lambda (t0: T).(\lambda (H3:
91 ((\forall (t2: T).((((eq T t0 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t0
92 t2) \to (sn3 c t2)))))).(\lambda (H4: ((\forall (t2: T).((((eq T t0 t2) \to
93 (\forall (P: Prop).P))) \to ((pr3 c t0 t2) \to (sn3 c (THead (Flat Cast) t1
94 t2))))))).(sn3_pr2_intro c (THead (Flat Cast) t1 t0) (\lambda (t2:
95 T).(\lambda (H5: (((eq T (THead (Flat Cast) t1 t0) t2) \to (\forall (P:
96 Prop).P)))).(\lambda (H6: (pr2 c (THead (Flat Cast) t1 t0) t2)).(let H7 \def
97 (pr2_gen_cast c t1 t0 t2 H6) in (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda
98 (t3: T).(eq T t2 (THead (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_:
99 T).(pr2 c t1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c t0 t3)))) (pr2 c
100 t0 t2) (sn3 c t2) (\lambda (H8: (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
101 T).(eq T t2 (THead (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_:
102 T).(pr2 c t1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c t0
103 t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
104 (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c t1 u2)))
105 (\lambda (_: T).(\lambda (t3: T).(pr2 c t0 t3))) (sn3 c t2) (\lambda (x0:
106 T).(\lambda (x1: T).(\lambda (H9: (eq T t2 (THead (Flat Cast) x0
107 x1))).(\lambda (H10: (pr2 c t1 x0)).(\lambda (H11: (pr2 c t0 x1)).(let H12
108 \def (eq_ind T t2 (\lambda (t3: T).((eq T (THead (Flat Cast) t1 t0) t3) \to
109 (\forall (P: Prop).P))) H5 (THead (Flat Cast) x0 x1) H9) in (eq_ind_r T
110 (THead (Flat Cast) x0 x1) (\lambda (t3: T).(sn3 c t3)) (let H_x \def
111 (term_dec x0 t1) in (let H13 \def H_x in (or_ind (eq T x0 t1) ((eq T x0 t1)
112 \to (\forall (P: Prop).P)) (sn3 c (THead (Flat Cast) x0 x1)) (\lambda (H14:
113 (eq T x0 t1)).(let H15 \def (eq_ind T x0 (\lambda (t3: T).((eq T (THead (Flat
114 Cast) t1 t0) (THead (Flat Cast) t3 x1)) \to (\forall (P: Prop).P))) H12 t1
115 H14) in (let H16 \def (eq_ind T x0 (\lambda (t3: T).(pr2 c t1 t3)) H10 t1
116 H14) in (eq_ind_r T t1 (\lambda (t3: T).(sn3 c (THead (Flat Cast) t3 x1)))
117 (let H_x0 \def (term_dec t0 x1) in (let H17 \def H_x0 in (or_ind (eq T t0 x1)
118 ((eq T t0 x1) \to (\forall (P: Prop).P)) (sn3 c (THead (Flat Cast) t1 x1))
119 (\lambda (H18: (eq T t0 x1)).(let H19 \def (eq_ind_r T x1 (\lambda (t3:
120 T).((eq T (THead (Flat Cast) t1 t0) (THead (Flat Cast) t1 t3)) \to (\forall
121 (P: Prop).P))) H15 t0 H18) in (let H20 \def (eq_ind_r T x1 (\lambda (t3:
122 T).(pr2 c t0 t3)) H11 t0 H18) in (eq_ind T t0 (\lambda (t3: T).(sn3 c (THead
123 (Flat Cast) t1 t3))) (H19 (refl_equal T (THead (Flat Cast) t1 t0)) (sn3 c
124 (THead (Flat Cast) t1 t0))) x1 H18)))) (\lambda (H18: (((eq T t0 x1) \to
125 (\forall (P: Prop).P)))).(H4 x1 H18 (pr3_pr2 c t0 x1 H11))) H17))) x0 H14))))
126 (\lambda (H14: (((eq T x0 t1) \to (\forall (P: Prop).P)))).(H1 x0 (\lambda
127 (H15: (eq T t1 x0)).(\lambda (P: Prop).(let H16 \def (eq_ind_r T x0 (\lambda
128 (t3: T).((eq T t3 t1) \to (\forall (P0: Prop).P0))) H14 t1 H15) in (let H17
129 \def (eq_ind_r T x0 (\lambda (t3: T).((eq T (THead (Flat Cast) t1 t0) (THead
130 (Flat Cast) t3 x1)) \to (\forall (P0: Prop).P0))) H12 t1 H15) in (let H18
131 \def (eq_ind_r T x0 (\lambda (t3: T).(pr2 c t1 t3)) H10 t1 H15) in (H16
132 (refl_equal T t1) P)))))) (pr3_pr2 c t1 x0 H10) x1 (let H_x0 \def (term_dec
133 t0 x1) in (let H15 \def H_x0 in (or_ind (eq T t0 x1) ((eq T t0 x1) \to
134 (\forall (P: Prop).P)) (sn3 c x1) (\lambda (H16: (eq T t0 x1)).(let H17 \def
135 (eq_ind_r T x1 (\lambda (t3: T).((eq T (THead (Flat Cast) t1 t0) (THead (Flat
136 Cast) x0 t3)) \to (\forall (P: Prop).P))) H12 t0 H16) in (let H18 \def
137 (eq_ind_r T x1 (\lambda (t3: T).(pr2 c t0 t3)) H11 t0 H16) in (eq_ind T t0
138 (\lambda (t3: T).(sn3 c t3)) (sn3_sing c t0 H3) x1 H16)))) (\lambda (H16:
139 (((eq T t0 x1) \to (\forall (P: Prop).P)))).(H3 x1 H16 (pr3_pr2 c t0 x1
140 H11))) H15))))) H13))) t2 H9))))))) H8)) (\lambda (H8: (pr2 c t0
141 t2)).(sn3_pr3_trans c t0 (sn3_sing c t0 H3) t2 (pr3_pr2 c t0 t2 H8)))
142 H7))))))))) t H2)))))) u H))).
144 theorem sn3_appl_lref:
145 \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (v:
146 T).((sn3 c v) \to (sn3 c (THead (Flat Appl) v (TLRef i)))))))
148 \lambda (c: C).(\lambda (i: nat).(\lambda (H: (nf2 c (TLRef i))).(\lambda
149 (v: T).(\lambda (H0: (sn3 c v)).(sn3_ind c (\lambda (t: T).(sn3 c (THead
150 (Flat Appl) t (TLRef i)))) (\lambda (t1: T).(\lambda (_: ((\forall (t2:
151 T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c
152 t2)))))).(\lambda (H2: ((\forall (t2: T).((((eq T t1 t2) \to (\forall (P:
153 Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c (THead (Flat Appl) t2 (TLRef
154 i)))))))).(sn3_pr2_intro c (THead (Flat Appl) t1 (TLRef i)) (\lambda (t2:
155 T).(\lambda (H3: (((eq T (THead (Flat Appl) t1 (TLRef i)) t2) \to (\forall
156 (P: Prop).P)))).(\lambda (H4: (pr2 c (THead (Flat Appl) t1 (TLRef i))
157 t2)).(let H5 \def (pr2_gen_appl c t1 (TLRef i) t2 H4) in (or3_ind (ex3_2 T T
158 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
159 (\lambda (u2: T).(\lambda (_: T).(pr2 c t1 u2))) (\lambda (_: T).(\lambda
160 (t3: T).(pr2 c (TLRef i) t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1:
161 T).(\lambda (_: T).(\lambda (_: T).(eq T (TLRef i) (THead (Bind Abst) y1
162 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3:
163 T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
164 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t1 u2))))) (\lambda (_:
165 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall
166 (u: T).(pr2 (CHead c (Bind b) u) z1 t3)))))))) (ex6_6 B T T T T T (\lambda
167 (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
168 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
169 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T
170 (TLRef i) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
171 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
172 t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
173 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
174 T).(\lambda (_: T).(pr2 c t1 u2))))))) (\lambda (_: B).(\lambda (y1:
175 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
176 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
177 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))))
178 (sn3 c t2) (\lambda (H6: (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T
179 t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c t1
180 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c (TLRef i) t3))))).(ex3_2_ind T
181 T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
182 (\lambda (u2: T).(\lambda (_: T).(pr2 c t1 u2))) (\lambda (_: T).(\lambda
183 (t3: T).(pr2 c (TLRef i) t3))) (sn3 c t2) (\lambda (x0: T).(\lambda (x1:
184 T).(\lambda (H7: (eq T t2 (THead (Flat Appl) x0 x1))).(\lambda (H8: (pr2 c t1
185 x0)).(\lambda (H9: (pr2 c (TLRef i) x1)).(let H10 \def (eq_ind T t2 (\lambda
186 (t: T).((eq T (THead (Flat Appl) t1 (TLRef i)) t) \to (\forall (P: Prop).P)))
187 H3 (THead (Flat Appl) x0 x1) H7) in (eq_ind_r T (THead (Flat Appl) x0 x1)
188 (\lambda (t: T).(sn3 c t)) (let H11 \def (eq_ind_r T x1 (\lambda (t: T).((eq
189 T (THead (Flat Appl) t1 (TLRef i)) (THead (Flat Appl) x0 t)) \to (\forall (P:
190 Prop).P))) H10 (TLRef i) (H x1 H9)) in (let H12 \def (eq_ind_r T x1 (\lambda
191 (t: T).(pr2 c (TLRef i) t)) H9 (TLRef i) (H x1 H9)) in (eq_ind T (TLRef i)
192 (\lambda (t: T).(sn3 c (THead (Flat Appl) x0 t))) (let H_x \def (term_dec t1
193 x0) in (let H13 \def H_x in (or_ind (eq T t1 x0) ((eq T t1 x0) \to (\forall
194 (P: Prop).P)) (sn3 c (THead (Flat Appl) x0 (TLRef i))) (\lambda (H14: (eq T
195 t1 x0)).(let H15 \def (eq_ind_r T x0 (\lambda (t: T).((eq T (THead (Flat
196 Appl) t1 (TLRef i)) (THead (Flat Appl) t (TLRef i))) \to (\forall (P:
197 Prop).P))) H11 t1 H14) in (let H16 \def (eq_ind_r T x0 (\lambda (t: T).(pr2 c
198 t1 t)) H8 t1 H14) in (eq_ind T t1 (\lambda (t: T).(sn3 c (THead (Flat Appl) t
199 (TLRef i)))) (H15 (refl_equal T (THead (Flat Appl) t1 (TLRef i))) (sn3 c
200 (THead (Flat Appl) t1 (TLRef i)))) x0 H14)))) (\lambda (H14: (((eq T t1 x0)
201 \to (\forall (P: Prop).P)))).(H2 x0 H14 (pr3_pr2 c t1 x0 H8))) H13))) x1 (H
202 x1 H9)))) t2 H7))))))) H6)) (\lambda (H6: (ex4_4 T T T T (\lambda (y1:
203 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (TLRef i) (THead
204 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
205 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
206 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t1 u2)))))
207 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall
208 (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t3))))))))).(ex4_4_ind T
209 T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
210 (TLRef i) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_:
211 T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3))))))
212 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t1
213 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3:
214 T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t3)))))))
215 (sn3 c t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3:
216 T).(\lambda (H7: (eq T (TLRef i) (THead (Bind Abst) x0 x1))).(\lambda (H8:
217 (eq T t2 (THead (Bind Abbr) x2 x3))).(\lambda (_: (pr2 c t1 x2)).(\lambda (_:
218 ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x1 x3))))).(let
219 H11 \def (eq_ind T t2 (\lambda (t: T).((eq T (THead (Flat Appl) t1 (TLRef i))
220 t) \to (\forall (P: Prop).P))) H3 (THead (Bind Abbr) x2 x3) H8) in (eq_ind_r
221 T (THead (Bind Abbr) x2 x3) (\lambda (t: T).(sn3 c t)) (let H12 \def (eq_ind
222 T (TLRef i) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
223 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _)
224 \Rightarrow False])) I (THead (Bind Abst) x0 x1) H7) in (False_ind (sn3 c
225 (THead (Bind Abbr) x2 x3)) H12)) t2 H8)))))))))) H6)) (\lambda (H6: (ex6_6 B
226 T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
227 T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
228 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
229 (_: T).(eq T (TLRef i) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda
230 (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq
231 T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
232 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
233 T).(\lambda (_: T).(pr2 c t1 u2))))))) (\lambda (_: B).(\lambda (y1:
234 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
235 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
236 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1
237 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda
238 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b
239 Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
240 T).(\lambda (_: T).(\lambda (_: T).(eq T (TLRef i) (THead (Bind b) y1
241 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2:
242 T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind b) y2 (THead (Flat
243 Appl) (lift (S O) O u2) z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda
244 (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t1 u2)))))))
245 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
246 T).(\lambda (y2: T).(pr2 c y1 y2))))))) (\lambda (b: B).(\lambda (_:
247 T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2
248 (CHead c (Bind b) y2) z1 z2))))))) (sn3 c t2) (\lambda (x0: B).(\lambda (x1:
249 T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda (x5:
250 T).(\lambda (_: (not (eq B x0 Abst))).(\lambda (H8: (eq T (TLRef i) (THead
251 (Bind x0) x1 x2))).(\lambda (H9: (eq T t2 (THead (Bind x0) x5 (THead (Flat
252 Appl) (lift (S O) O x4) x3)))).(\lambda (_: (pr2 c t1 x4)).(\lambda (_: (pr2
253 c x1 x5)).(\lambda (_: (pr2 (CHead c (Bind x0) x5) x2 x3)).(let H13 \def
254 (eq_ind T t2 (\lambda (t: T).((eq T (THead (Flat Appl) t1 (TLRef i)) t) \to
255 (\forall (P: Prop).P))) H3 (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O)
256 O x4) x3)) H9) in (eq_ind_r T (THead (Bind x0) x5 (THead (Flat Appl) (lift (S
257 O) O x4) x3)) (\lambda (t: T).(sn3 c t)) (let H14 \def (eq_ind T (TLRef i)
258 (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort _)
259 \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
260 False])) I (THead (Bind x0) x1 x2) H8) in (False_ind (sn3 c (THead (Bind x0)
261 x5 (THead (Flat Appl) (lift (S O) O x4) x3))) H14)) t2 H9)))))))))))))) H6))
262 H5))))))))) v H0))))).
264 theorem sn3_appl_cast:
265 \forall (c: C).(\forall (v: T).(\forall (u: T).((sn3 c (THead (Flat Appl) v
266 u)) \to (\forall (t: T).((sn3 c (THead (Flat Appl) v t)) \to (sn3 c (THead
267 (Flat Appl) v (THead (Flat Cast) u t))))))))
269 \lambda (c: C).(\lambda (v: T).(\lambda (u: T).(\lambda (H: (sn3 c (THead
270 (Flat Appl) v u))).(insert_eq T (THead (Flat Appl) v u) (\lambda (t: T).(sn3
271 c t)) (\forall (t: T).((sn3 c (THead (Flat Appl) v t)) \to (sn3 c (THead
272 (Flat Appl) v (THead (Flat Cast) u t))))) (\lambda (y: T).(\lambda (H0: (sn3
273 c y)).(unintro T u (\lambda (t: T).((eq T y (THead (Flat Appl) v t)) \to
274 (\forall (t0: T).((sn3 c (THead (Flat Appl) v t0)) \to (sn3 c (THead (Flat
275 Appl) v (THead (Flat Cast) t t0))))))) (unintro T v (\lambda (t: T).(\forall
276 (x: T).((eq T y (THead (Flat Appl) t x)) \to (\forall (t0: T).((sn3 c (THead
277 (Flat Appl) t t0)) \to (sn3 c (THead (Flat Appl) t (THead (Flat Cast) x
278 t0)))))))) (sn3_ind c (\lambda (t: T).(\forall (x: T).(\forall (x0: T).((eq T
279 t (THead (Flat Appl) x x0)) \to (\forall (t0: T).((sn3 c (THead (Flat Appl) x
280 t0)) \to (sn3 c (THead (Flat Appl) x (THead (Flat Cast) x0 t0)))))))))
281 (\lambda (t1: T).(\lambda (H1: ((\forall (t2: T).((((eq T t1 t2) \to (\forall
282 (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c t2)))))).(\lambda (H2: ((\forall
283 (t2: T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to
284 (\forall (x: T).(\forall (x0: T).((eq T t2 (THead (Flat Appl) x x0)) \to
285 (\forall (t: T).((sn3 c (THead (Flat Appl) x t)) \to (sn3 c (THead (Flat
286 Appl) x (THead (Flat Cast) x0 t))))))))))))).(\lambda (x: T).(\lambda (x0:
287 T).(\lambda (H3: (eq T t1 (THead (Flat Appl) x x0))).(\lambda (t: T).(\lambda
288 (H4: (sn3 c (THead (Flat Appl) x t))).(insert_eq T (THead (Flat Appl) x t)
289 (\lambda (t0: T).(sn3 c t0)) (sn3 c (THead (Flat Appl) x (THead (Flat Cast)
290 x0 t))) (\lambda (y0: T).(\lambda (H5: (sn3 c y0)).(unintro T t (\lambda (t0:
291 T).((eq T y0 (THead (Flat Appl) x t0)) \to (sn3 c (THead (Flat Appl) x (THead
292 (Flat Cast) x0 t0))))) (sn3_ind c (\lambda (t0: T).(\forall (x1: T).((eq T t0
293 (THead (Flat Appl) x x1)) \to (sn3 c (THead (Flat Appl) x (THead (Flat Cast)
294 x0 x1)))))) (\lambda (t0: T).(\lambda (H6: ((\forall (t2: T).((((eq T t0 t2)
295 \to (\forall (P: Prop).P))) \to ((pr3 c t0 t2) \to (sn3 c t2)))))).(\lambda
296 (H7: ((\forall (t2: T).((((eq T t0 t2) \to (\forall (P: Prop).P))) \to ((pr3
297 c t0 t2) \to (\forall (x1: T).((eq T t2 (THead (Flat Appl) x x1)) \to (sn3 c
298 (THead (Flat Appl) x (THead (Flat Cast) x0 x1)))))))))).(\lambda (x1:
299 T).(\lambda (H8: (eq T t0 (THead (Flat Appl) x x1))).(let H9 \def (eq_ind T
300 t0 (\lambda (t2: T).(\forall (t3: T).((((eq T t2 t3) \to (\forall (P:
301 Prop).P))) \to ((pr3 c t2 t3) \to (\forall (x2: T).((eq T t3 (THead (Flat
302 Appl) x x2)) \to (sn3 c (THead (Flat Appl) x (THead (Flat Cast) x0
303 x2))))))))) H7 (THead (Flat Appl) x x1) H8) in (let H10 \def (eq_ind T t0
304 (\lambda (t2: T).(\forall (t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P)))
305 \to ((pr3 c t2 t3) \to (sn3 c t3))))) H6 (THead (Flat Appl) x x1) H8) in (let
306 H11 \def (eq_ind T t1 (\lambda (t2: T).(\forall (t3: T).((((eq T t2 t3) \to
307 (\forall (P: Prop).P))) \to ((pr3 c t2 t3) \to (\forall (x2: T).(\forall (x3:
308 T).((eq T t3 (THead (Flat Appl) x2 x3)) \to (\forall (t4: T).((sn3 c (THead
309 (Flat Appl) x2 t4)) \to (sn3 c (THead (Flat Appl) x2 (THead (Flat Cast) x3
310 t4)))))))))))) H2 (THead (Flat Appl) x x0) H3) in (let H12 \def (eq_ind T t1
311 (\lambda (t2: T).(\forall (t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P)))
312 \to ((pr3 c t2 t3) \to (sn3 c t3))))) H1 (THead (Flat Appl) x x0) H3) in
313 (sn3_pr2_intro c (THead (Flat Appl) x (THead (Flat Cast) x0 x1)) (\lambda
314 (t2: T).(\lambda (H13: (((eq T (THead (Flat Appl) x (THead (Flat Cast) x0
315 x1)) t2) \to (\forall (P: Prop).P)))).(\lambda (H14: (pr2 c (THead (Flat
316 Appl) x (THead (Flat Cast) x0 x1)) t2)).(let H15 \def (pr2_gen_appl c x
317 (THead (Flat Cast) x0 x1) t2 H14) in (or3_ind (ex3_2 T T (\lambda (u2:
318 T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
319 T).(\lambda (_: T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c
320 (THead (Flat Cast) x0 x1) t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
321 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Cast) x0 x1)
322 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
323 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
324 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
325 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b:
326 B).(\forall (u0: T).(pr2 (CHead c (Bind b) u0) z1 t3)))))))) (ex6_6 B T T T T
327 T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
328 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
329 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq
330 T (THead (Flat Cast) x0 x1) (THead (Bind b) y1 z1)))))))) (\lambda (b:
331 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
332 (y2: T).(eq T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2)
333 z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
334 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_:
335 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
336 (y2: T).(pr2 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
337 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b)
338 y2) z1 z2)))))))) (sn3 c t2) (\lambda (H16: (ex3_2 T T (\lambda (u2:
339 T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
340 T).(\lambda (_: T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c
341 (THead (Flat Cast) x0 x1) t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda
342 (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_:
343 T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c (THead (Flat Cast)
344 x0 x1) t3))) (sn3 c t2) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H17: (eq
345 T t2 (THead (Flat Appl) x2 x3))).(\lambda (H18: (pr2 c x x2)).(\lambda (H19:
346 (pr2 c (THead (Flat Cast) x0 x1) x3)).(let H20 \def (eq_ind T t2 (\lambda
347 (t3: T).((eq T (THead (Flat Appl) x (THead (Flat Cast) x0 x1)) t3) \to
348 (\forall (P: Prop).P))) H13 (THead (Flat Appl) x2 x3) H17) in (eq_ind_r T
349 (THead (Flat Appl) x2 x3) (\lambda (t3: T).(sn3 c t3)) (let H21 \def
350 (pr2_gen_cast c x0 x1 x3 H19) in (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda
351 (t3: T).(eq T x3 (THead (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_:
352 T).(pr2 c x0 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c x1 t3)))) (pr2 c
353 x1 x3) (sn3 c (THead (Flat Appl) x2 x3)) (\lambda (H22: (ex3_2 T T (\lambda
354 (u2: T).(\lambda (t3: T).(eq T x3 (THead (Flat Cast) u2 t3)))) (\lambda (u2:
355 T).(\lambda (_: T).(pr2 c x0 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c x1
356 t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq T x3 (THead
357 (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2)))
358 (\lambda (_: T).(\lambda (t3: T).(pr2 c x1 t3))) (sn3 c (THead (Flat Appl) x2
359 x3)) (\lambda (x4: T).(\lambda (x5: T).(\lambda (H23: (eq T x3 (THead (Flat
360 Cast) x4 x5))).(\lambda (H24: (pr2 c x0 x4)).(\lambda (H25: (pr2 c x1
361 x5)).(let H26 \def (eq_ind T x3 (\lambda (t3: T).((eq T (THead (Flat Appl) x
362 (THead (Flat Cast) x0 x1)) (THead (Flat Appl) x2 t3)) \to (\forall (P:
363 Prop).P))) H20 (THead (Flat Cast) x4 x5) H23) in (eq_ind_r T (THead (Flat
364 Cast) x4 x5) (\lambda (t3: T).(sn3 c (THead (Flat Appl) x2 t3))) (let H_x
365 \def (term_dec (THead (Flat Appl) x x0) (THead (Flat Appl) x2 x4)) in (let
366 H27 \def H_x in (or_ind (eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x2
367 x4)) ((eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x2 x4)) \to (\forall
368 (P: Prop).P)) (sn3 c (THead (Flat Appl) x2 (THead (Flat Cast) x4 x5)))
369 (\lambda (H28: (eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x2
370 x4))).(let H29 \def (f_equal T T (\lambda (e: T).(match e in T return
371 (\lambda (_: T).T) with [(TSort _) \Rightarrow x | (TLRef _) \Rightarrow x |
372 (THead _ t3 _) \Rightarrow t3])) (THead (Flat Appl) x x0) (THead (Flat Appl)
373 x2 x4) H28) in ((let H30 \def (f_equal T T (\lambda (e: T).(match e in T
374 return (\lambda (_: T).T) with [(TSort _) \Rightarrow x0 | (TLRef _)
375 \Rightarrow x0 | (THead _ _ t3) \Rightarrow t3])) (THead (Flat Appl) x x0)
376 (THead (Flat Appl) x2 x4) H28) in (\lambda (H31: (eq T x x2)).(let H32 \def
377 (eq_ind_r T x4 (\lambda (t3: T).((eq T (THead (Flat Appl) x (THead (Flat
378 Cast) x0 x1)) (THead (Flat Appl) x2 (THead (Flat Cast) t3 x5))) \to (\forall
379 (P: Prop).P))) H26 x0 H30) in (let H33 \def (eq_ind_r T x4 (\lambda (t3:
380 T).(pr2 c x0 t3)) H24 x0 H30) in (eq_ind T x0 (\lambda (t3: T).(sn3 c (THead
381 (Flat Appl) x2 (THead (Flat Cast) t3 x5)))) (let H34 \def (eq_ind_r T x2
382 (\lambda (t3: T).((eq T (THead (Flat Appl) x (THead (Flat Cast) x0 x1))
383 (THead (Flat Appl) t3 (THead (Flat Cast) x0 x5))) \to (\forall (P: Prop).P)))
384 H32 x H31) in (let H35 \def (eq_ind_r T x2 (\lambda (t3: T).(pr2 c x t3)) H18
385 x H31) in (eq_ind T x (\lambda (t3: T).(sn3 c (THead (Flat Appl) t3 (THead
386 (Flat Cast) x0 x5)))) (let H_x0 \def (term_dec (THead (Flat Appl) x x1)
387 (THead (Flat Appl) x x5)) in (let H36 \def H_x0 in (or_ind (eq T (THead (Flat
388 Appl) x x1) (THead (Flat Appl) x x5)) ((eq T (THead (Flat Appl) x x1) (THead
389 (Flat Appl) x x5)) \to (\forall (P: Prop).P)) (sn3 c (THead (Flat Appl) x
390 (THead (Flat Cast) x0 x5))) (\lambda (H37: (eq T (THead (Flat Appl) x x1)
391 (THead (Flat Appl) x x5))).(let H38 \def (f_equal T T (\lambda (e: T).(match
392 e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow x1 | (TLRef _)
393 \Rightarrow x1 | (THead _ _ t3) \Rightarrow t3])) (THead (Flat Appl) x x1)
394 (THead (Flat Appl) x x5) H37) in (let H39 \def (eq_ind_r T x5 (\lambda (t3:
395 T).((eq T (THead (Flat Appl) x (THead (Flat Cast) x0 x1)) (THead (Flat Appl)
396 x (THead (Flat Cast) x0 t3))) \to (\forall (P: Prop).P))) H34 x1 H38) in (let
397 H40 \def (eq_ind_r T x5 (\lambda (t3: T).(pr2 c x1 t3)) H25 x1 H38) in
398 (eq_ind T x1 (\lambda (t3: T).(sn3 c (THead (Flat Appl) x (THead (Flat Cast)
399 x0 t3)))) (H39 (refl_equal T (THead (Flat Appl) x (THead (Flat Cast) x0 x1)))
400 (sn3 c (THead (Flat Appl) x (THead (Flat Cast) x0 x1)))) x5 H38))))) (\lambda
401 (H37: (((eq T (THead (Flat Appl) x x1) (THead (Flat Appl) x x5)) \to (\forall
402 (P: Prop).P)))).(H9 (THead (Flat Appl) x x5) H37 (pr3_pr2 c (THead (Flat
403 Appl) x x1) (THead (Flat Appl) x x5) (pr2_thin_dx c x1 x5 H25 x Appl)) x5
404 (refl_equal T (THead (Flat Appl) x x5)))) H36))) x2 H31))) x4 H30))))) H29)))
405 (\lambda (H28: (((eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x2 x4))
406 \to (\forall (P: Prop).P)))).(let H_x0 \def (term_dec (THead (Flat Appl) x
407 x1) (THead (Flat Appl) x2 x5)) in (let H29 \def H_x0 in (or_ind (eq T (THead
408 (Flat Appl) x x1) (THead (Flat Appl) x2 x5)) ((eq T (THead (Flat Appl) x x1)
409 (THead (Flat Appl) x2 x5)) \to (\forall (P: Prop).P)) (sn3 c (THead (Flat
410 Appl) x2 (THead (Flat Cast) x4 x5))) (\lambda (H30: (eq T (THead (Flat Appl)
411 x x1) (THead (Flat Appl) x2 x5))).(let H31 \def (f_equal T T (\lambda (e:
412 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow x |
413 (TLRef _) \Rightarrow x | (THead _ t3 _) \Rightarrow t3])) (THead (Flat Appl)
414 x x1) (THead (Flat Appl) x2 x5) H30) in ((let H32 \def (f_equal T T (\lambda
415 (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow x1
416 | (TLRef _) \Rightarrow x1 | (THead _ _ t3) \Rightarrow t3])) (THead (Flat
417 Appl) x x1) (THead (Flat Appl) x2 x5) H30) in (\lambda (H33: (eq T x
418 x2)).(let H34 \def (eq_ind_r T x5 (\lambda (t3: T).(pr2 c x1 t3)) H25 x1 H32)
419 in (eq_ind T x1 (\lambda (t3: T).(sn3 c (THead (Flat Appl) x2 (THead (Flat
420 Cast) x4 t3)))) (let H35 \def (eq_ind_r T x2 (\lambda (t3: T).((eq T (THead
421 (Flat Appl) x x0) (THead (Flat Appl) t3 x4)) \to (\forall (P: Prop).P))) H28
422 x H33) in (let H36 \def (eq_ind_r T x2 (\lambda (t3: T).(pr2 c x t3)) H18 x
423 H33) in (eq_ind T x (\lambda (t3: T).(sn3 c (THead (Flat Appl) t3 (THead
424 (Flat Cast) x4 x1)))) (H11 (THead (Flat Appl) x x4) H35 (pr3_pr2 c (THead
425 (Flat Appl) x x0) (THead (Flat Appl) x x4) (pr2_thin_dx c x0 x4 H24 x Appl))
426 x x4 (refl_equal T (THead (Flat Appl) x x4)) x1 (sn3_sing c (THead (Flat
427 Appl) x x1) H10)) x2 H33))) x5 H32)))) H31))) (\lambda (H30: (((eq T (THead
428 (Flat Appl) x x1) (THead (Flat Appl) x2 x5)) \to (\forall (P:
429 Prop).P)))).(H11 (THead (Flat Appl) x2 x4) H28 (pr3_flat c x x2 (pr3_pr2 c x
430 x2 H18) x0 x4 (pr3_pr2 c x0 x4 H24) Appl) x2 x4 (refl_equal T (THead (Flat
431 Appl) x2 x4)) x5 (H10 (THead (Flat Appl) x2 x5) H30 (pr3_flat c x x2 (pr3_pr2
432 c x x2 H18) x1 x5 (pr3_pr2 c x1 x5 H25) Appl)))) H29)))) H27))) x3 H23)))))))
433 H22)) (\lambda (H22: (pr2 c x1 x3)).(let H_x \def (term_dec (THead (Flat
434 Appl) x x1) (THead (Flat Appl) x2 x3)) in (let H23 \def H_x in (or_ind (eq T
435 (THead (Flat Appl) x x1) (THead (Flat Appl) x2 x3)) ((eq T (THead (Flat Appl)
436 x x1) (THead (Flat Appl) x2 x3)) \to (\forall (P: Prop).P)) (sn3 c (THead
437 (Flat Appl) x2 x3)) (\lambda (H24: (eq T (THead (Flat Appl) x x1) (THead
438 (Flat Appl) x2 x3))).(let H25 \def (f_equal T T (\lambda (e: T).(match e in T
439 return (\lambda (_: T).T) with [(TSort _) \Rightarrow x | (TLRef _)
440 \Rightarrow x | (THead _ t3 _) \Rightarrow t3])) (THead (Flat Appl) x x1)
441 (THead (Flat Appl) x2 x3) H24) in ((let H26 \def (f_equal T T (\lambda (e:
442 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow x1 |
443 (TLRef _) \Rightarrow x1 | (THead _ _ t3) \Rightarrow t3])) (THead (Flat
444 Appl) x x1) (THead (Flat Appl) x2 x3) H24) in (\lambda (H27: (eq T x
445 x2)).(let H28 \def (eq_ind_r T x3 (\lambda (t3: T).(pr2 c x1 t3)) H22 x1 H26)
446 in (let H29 \def (eq_ind_r T x3 (\lambda (t3: T).((eq T (THead (Flat Appl) x
447 (THead (Flat Cast) x0 x1)) (THead (Flat Appl) x2 t3)) \to (\forall (P:
448 Prop).P))) H20 x1 H26) in (eq_ind T x1 (\lambda (t3: T).(sn3 c (THead (Flat
449 Appl) x2 t3))) (let H30 \def (eq_ind_r T x2 (\lambda (t3: T).((eq T (THead
450 (Flat Appl) x (THead (Flat Cast) x0 x1)) (THead (Flat Appl) t3 x1)) \to
451 (\forall (P: Prop).P))) H29 x H27) in (let H31 \def (eq_ind_r T x2 (\lambda
452 (t3: T).(pr2 c x t3)) H18 x H27) in (eq_ind T x (\lambda (t3: T).(sn3 c
453 (THead (Flat Appl) t3 x1))) (sn3_sing c (THead (Flat Appl) x x1) H10) x2
454 H27))) x3 H26))))) H25))) (\lambda (H24: (((eq T (THead (Flat Appl) x x1)
455 (THead (Flat Appl) x2 x3)) \to (\forall (P: Prop).P)))).(H10 (THead (Flat
456 Appl) x2 x3) H24 (pr3_flat c x x2 (pr3_pr2 c x x2 H18) x1 x3 (pr3_pr2 c x1 x3
457 H22) Appl))) H23)))) H21)) t2 H17))))))) H16)) (\lambda (H16: (ex4_4 T T T T
458 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
459 (THead (Flat Cast) x0 x1) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
460 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
461 Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
462 (_: T).(pr2 c x u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
463 T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b)
464 u0) z1 t3))))))))).(ex4_4_ind T T T T (\lambda (y1: T).(\lambda (z1:
465 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Cast) x0 x1) (THead
466 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
467 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
468 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
469 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b:
470 B).(\forall (u0: T).(pr2 (CHead c (Bind b) u0) z1 t3))))))) (sn3 c t2)
471 (\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda
472 (H17: (eq T (THead (Flat Cast) x0 x1) (THead (Bind Abst) x2 x3))).(\lambda
473 (H18: (eq T t2 (THead (Bind Abbr) x4 x5))).(\lambda (_: (pr2 c x
474 x4)).(\lambda (_: ((\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b)
475 u0) x3 x5))))).(let H21 \def (eq_ind T t2 (\lambda (t3: T).((eq T (THead
476 (Flat Appl) x (THead (Flat Cast) x0 x1)) t3) \to (\forall (P: Prop).P))) H13
477 (THead (Bind Abbr) x4 x5) H18) in (eq_ind_r T (THead (Bind Abbr) x4 x5)
478 (\lambda (t3: T).(sn3 c t3)) (let H22 \def (eq_ind T (THead (Flat Cast) x0
479 x1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
480 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
481 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
482 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abst) x2
483 x3) H17) in (False_ind (sn3 c (THead (Bind Abbr) x4 x5)) H22)) t2
484 H18)))))))))) H16)) (\lambda (H16: (ex6_6 B T T T T T (\lambda (b:
485 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
486 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
487 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat
488 Cast) x0 x1) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
489 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
490 t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
491 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
492 T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1:
493 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
494 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
495 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1
496 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda
497 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b
498 Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
499 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Cast) x0 x1) (THead
500 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
501 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
502 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
503 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
504 (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
505 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
506 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
507 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))) (sn3 c t2)
508 (\lambda (x2: B).(\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda
509 (x6: T).(\lambda (x7: T).(\lambda (_: (not (eq B x2 Abst))).(\lambda (H18:
510 (eq T (THead (Flat Cast) x0 x1) (THead (Bind x2) x3 x4))).(\lambda (H19: (eq
511 T t2 (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) O x6) x5)))).(\lambda
512 (_: (pr2 c x x6)).(\lambda (_: (pr2 c x3 x7)).(\lambda (_: (pr2 (CHead c
513 (Bind x2) x7) x4 x5)).(let H23 \def (eq_ind T t2 (\lambda (t3: T).((eq T
514 (THead (Flat Appl) x (THead (Flat Cast) x0 x1)) t3) \to (\forall (P:
515 Prop).P))) H13 (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) O x6) x5))
516 H19) in (eq_ind_r T (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) O x6)
517 x5)) (\lambda (t3: T).(sn3 c t3)) (let H24 \def (eq_ind T (THead (Flat Cast)
518 x0 x1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
519 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
520 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
521 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind x2) x3 x4)
522 H18) in (False_ind (sn3 c (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O)
523 O x6) x5))) H24)) t2 H19)))))))))))))) H16)) H15))))))))))))))) y0 H5))))
524 H4))))))))) y H0))))) H)))).
526 theorem sn3_appl_appl:
527 \forall (v1: T).(\forall (t1: T).(let u1 \def (THead (Flat Appl) v1 t1) in
528 (\forall (c: C).((sn3 c u1) \to (\forall (v2: T).((sn3 c v2) \to (((\forall
529 (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to (\forall (P: Prop).P))) \to
530 (sn3 c (THead (Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2
533 \lambda (v1: T).(\lambda (t1: T).(let u1 \def (THead (Flat Appl) v1 t1) in
534 (\lambda (c: C).(\lambda (H: (sn3 c (THead (Flat Appl) v1 t1))).(insert_eq T
535 (THead (Flat Appl) v1 t1) (\lambda (t: T).(sn3 c t)) (\forall (v2: T).((sn3 c
536 v2) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) v1 t1) u2) \to ((((iso
537 (THead (Flat Appl) v1 t1) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead
538 (Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2 (THead (Flat Appl)
539 v1 t1)))))) (\lambda (y: T).(\lambda (H0: (sn3 c y)).(unintro T t1 (\lambda
540 (t: T).((eq T y (THead (Flat Appl) v1 t)) \to (\forall (v2: T).((sn3 c v2)
541 \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) v1 t) u2) \to ((((iso
542 (THead (Flat Appl) v1 t) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead
543 (Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2 (THead (Flat Appl)
544 v1 t)))))))) (unintro T v1 (\lambda (t: T).(\forall (x: T).((eq T y (THead
545 (Flat Appl) t x)) \to (\forall (v2: T).((sn3 c v2) \to (((\forall (u2:
546 T).((pr3 c (THead (Flat Appl) t x) u2) \to ((((iso (THead (Flat Appl) t x)
547 u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to
548 (sn3 c (THead (Flat Appl) v2 (THead (Flat Appl) t x))))))))) (sn3_ind c
549 (\lambda (t: T).(\forall (x: T).(\forall (x0: T).((eq T t (THead (Flat Appl)
550 x x0)) \to (\forall (v2: T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c (THead
551 (Flat Appl) x x0) u2) \to ((((iso (THead (Flat Appl) x x0) u2) \to (\forall
552 (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to (sn3 c (THead
553 (Flat Appl) v2 (THead (Flat Appl) x x0)))))))))) (\lambda (t2: T).(\lambda
554 (H1: ((\forall (t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P))) \to ((pr3
555 c t2 t3) \to (sn3 c t3)))))).(\lambda (H2: ((\forall (t3: T).((((eq T t2 t3)
556 \to (\forall (P: Prop).P))) \to ((pr3 c t2 t3) \to (\forall (x: T).(\forall
557 (x0: T).((eq T t3 (THead (Flat Appl) x x0)) \to (\forall (v2: T).((sn3 c v2)
558 \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x x0) u2) \to ((((iso
559 (THead (Flat Appl) x x0) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead
560 (Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2 (THead (Flat Appl) x
561 x0)))))))))))))).(\lambda (x: T).(\lambda (x0: T).(\lambda (H3: (eq T t2
562 (THead (Flat Appl) x x0))).(\lambda (v2: T).(\lambda (H4: (sn3 c
563 v2)).(sn3_ind c (\lambda (t: T).(((\forall (u2: T).((pr3 c (THead (Flat Appl)
564 x x0) u2) \to ((((iso (THead (Flat Appl) x x0) u2) \to (\forall (P:
565 Prop).P))) \to (sn3 c (THead (Flat Appl) t u2)))))) \to (sn3 c (THead (Flat
566 Appl) t (THead (Flat Appl) x x0))))) (\lambda (t0: T).(\lambda (H5: ((\forall
567 (t3: T).((((eq T t0 t3) \to (\forall (P: Prop).P))) \to ((pr3 c t0 t3) \to
568 (sn3 c t3)))))).(\lambda (H6: ((\forall (t3: T).((((eq T t0 t3) \to (\forall
569 (P: Prop).P))) \to ((pr3 c t0 t3) \to (((\forall (u2: T).((pr3 c (THead (Flat
570 Appl) x x0) u2) \to ((((iso (THead (Flat Appl) x x0) u2) \to (\forall (P:
571 Prop).P))) \to (sn3 c (THead (Flat Appl) t3 u2)))))) \to (sn3 c (THead (Flat
572 Appl) t3 (THead (Flat Appl) x x0))))))))).(\lambda (H7: ((\forall (u2:
573 T).((pr3 c (THead (Flat Appl) x x0) u2) \to ((((iso (THead (Flat Appl) x x0)
574 u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) t0
575 u2))))))).(let H8 \def (eq_ind T t2 (\lambda (t: T).(\forall (t3: T).((((eq T
576 t t3) \to (\forall (P: Prop).P))) \to ((pr3 c t t3) \to (\forall (x1:
577 T).(\forall (x2: T).((eq T t3 (THead (Flat Appl) x1 x2)) \to (\forall (v3:
578 T).((sn3 c v3) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x1 x2) u2)
579 \to ((((iso (THead (Flat Appl) x1 x2) u2) \to (\forall (P: Prop).P))) \to
580 (sn3 c (THead (Flat Appl) v3 u2)))))) \to (sn3 c (THead (Flat Appl) v3 (THead
581 (Flat Appl) x1 x2))))))))))))) H2 (THead (Flat Appl) x x0) H3) in (let H9
582 \def (eq_ind T t2 (\lambda (t: T).(\forall (t3: T).((((eq T t t3) \to
583 (\forall (P: Prop).P))) \to ((pr3 c t t3) \to (sn3 c t3))))) H1 (THead (Flat
584 Appl) x x0) H3) in (sn3_pr2_intro c (THead (Flat Appl) t0 (THead (Flat Appl)
585 x x0)) (\lambda (t3: T).(\lambda (H10: (((eq T (THead (Flat Appl) t0 (THead
586 (Flat Appl) x x0)) t3) \to (\forall (P: Prop).P)))).(\lambda (H11: (pr2 c
587 (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t3)).(let H12 \def
588 (pr2_gen_appl c t0 (THead (Flat Appl) x x0) t3 H11) in (or3_ind (ex3_2 T T
589 (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 t4))))
590 (\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2))) (\lambda (_: T).(\lambda
591 (t4: T).(pr2 c (THead (Flat Appl) x x0) t4)))) (ex4_4 T T T T (\lambda (y1:
592 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Appl)
593 x x0) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda
594 (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
595 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2)))))
596 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall
597 (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4)))))))) (ex6_6 B T T T
598 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
599 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
600 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq
601 T (THead (Flat Appl) x x0) (THead (Bind b) y1 z1)))))))) (\lambda (b:
602 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
603 (y2: T).(eq T t3 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2)
604 z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
605 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2))))))) (\lambda (_:
606 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
607 (y2: T).(pr2 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
608 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b)
609 y2) z1 z2)))))))) (sn3 c t3) (\lambda (H13: (ex3_2 T T (\lambda (u2:
610 T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2:
611 T).(\lambda (_: T).(pr2 c t0 u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c
612 (THead (Flat Appl) x x0) t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda
613 (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_:
614 T).(pr2 c t0 u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c (THead (Flat Appl)
615 x x0) t4))) (sn3 c t3) (\lambda (x1: T).(\lambda (x2: T).(\lambda (H14: (eq T
616 t3 (THead (Flat Appl) x1 x2))).(\lambda (H15: (pr2 c t0 x1)).(\lambda (H16:
617 (pr2 c (THead (Flat Appl) x x0) x2)).(let H17 \def (eq_ind T t3 (\lambda (t:
618 T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t) \to (\forall (P:
619 Prop).P))) H10 (THead (Flat Appl) x1 x2) H14) in (eq_ind_r T (THead (Flat
620 Appl) x1 x2) (\lambda (t: T).(sn3 c t)) (let H18 \def (pr2_gen_appl c x x0 x2
621 H16) in (or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T x2 (THead
622 (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
623 (\lambda (_: T).(\lambda (t4: T).(pr2 c x0 t4)))) (ex4_4 T T T T (\lambda
624 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T x0 (THead
625 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
626 T).(\lambda (t4: T).(eq T x2 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
627 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
628 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b:
629 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4)))))))) (ex6_6 B T T T T T
630 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
631 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
632 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T x0
633 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
634 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T x2 (THead (Bind
635 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
636 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
637 (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
638 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
639 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
640 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))) (sn3 c
641 (THead (Flat Appl) x1 x2)) (\lambda (H19: (ex3_2 T T (\lambda (u2:
642 T).(\lambda (t4: T).(eq T x2 (THead (Flat Appl) u2 t4)))) (\lambda (u2:
643 T).(\lambda (_: T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c x0
644 t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t4: T).(eq T x2 (THead
645 (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
646 (\lambda (_: T).(\lambda (t4: T).(pr2 c x0 t4))) (sn3 c (THead (Flat Appl) x1
647 x2)) (\lambda (x3: T).(\lambda (x4: T).(\lambda (H20: (eq T x2 (THead (Flat
648 Appl) x3 x4))).(\lambda (H21: (pr2 c x x3)).(\lambda (H22: (pr2 c x0
649 x4)).(let H23 \def (eq_ind T x2 (\lambda (t: T).((eq T (THead (Flat Appl) t0
650 (THead (Flat Appl) x x0)) (THead (Flat Appl) x1 t)) \to (\forall (P:
651 Prop).P))) H17 (THead (Flat Appl) x3 x4) H20) in (eq_ind_r T (THead (Flat
652 Appl) x3 x4) (\lambda (t: T).(sn3 c (THead (Flat Appl) x1 t))) (let H_x \def
653 (term_dec (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4)) in (let H24
654 \def H_x in (or_ind (eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4))
655 ((eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4)) \to (\forall (P:
656 Prop).P)) (sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))) (\lambda
657 (H25: (eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4))).(let H26
658 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
659 with [(TSort _) \Rightarrow x | (TLRef _) \Rightarrow x | (THead _ t _)
660 \Rightarrow t])) (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4) H25) in
661 ((let H27 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_:
662 T).T) with [(TSort _) \Rightarrow x0 | (TLRef _) \Rightarrow x0 | (THead _ _
663 t) \Rightarrow t])) (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4) H25)
664 in (\lambda (H28: (eq T x x3)).(let H29 \def (eq_ind_r T x4 (\lambda (t:
665 T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) (THead (Flat Appl)
666 x1 (THead (Flat Appl) x3 t))) \to (\forall (P: Prop).P))) H23 x0 H27) in (let
667 H30 \def (eq_ind_r T x4 (\lambda (t: T).(pr2 c x0 t)) H22 x0 H27) in (eq_ind
668 T x0 (\lambda (t: T).(sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 t))))
669 (let H31 \def (eq_ind_r T x3 (\lambda (t: T).((eq T (THead (Flat Appl) t0
670 (THead (Flat Appl) x x0)) (THead (Flat Appl) x1 (THead (Flat Appl) t x0)))
671 \to (\forall (P: Prop).P))) H29 x H28) in (let H32 \def (eq_ind_r T x3
672 (\lambda (t: T).(pr2 c x t)) H21 x H28) in (eq_ind T x (\lambda (t: T).(sn3 c
673 (THead (Flat Appl) x1 (THead (Flat Appl) t x0)))) (let H_x0 \def (term_dec t0
674 x1) in (let H33 \def H_x0 in (or_ind (eq T t0 x1) ((eq T t0 x1) \to (\forall
675 (P: Prop).P)) (sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x x0)))
676 (\lambda (H34: (eq T t0 x1)).(let H35 \def (eq_ind_r T x1 (\lambda (t:
677 T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) (THead (Flat Appl)
678 t (THead (Flat Appl) x x0))) \to (\forall (P: Prop).P))) H31 t0 H34) in (let
679 H36 \def (eq_ind_r T x1 (\lambda (t: T).(pr2 c t0 t)) H15 t0 H34) in (eq_ind
680 T t0 (\lambda (t: T).(sn3 c (THead (Flat Appl) t (THead (Flat Appl) x x0))))
681 (H35 (refl_equal T (THead (Flat Appl) t0 (THead (Flat Appl) x x0))) (sn3 c
682 (THead (Flat Appl) t0 (THead (Flat Appl) x x0)))) x1 H34)))) (\lambda (H34:
683 (((eq T t0 x1) \to (\forall (P: Prop).P)))).(H6 x1 H34 (pr3_pr2 c t0 x1 H15)
684 (\lambda (u2: T).(\lambda (H35: (pr3 c (THead (Flat Appl) x x0) u2)).(\lambda
685 (H36: (((iso (THead (Flat Appl) x x0) u2) \to (\forall (P:
686 Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t0 u2) (H7 u2 H35 H36) (THead
687 (Flat Appl) x1 u2) (pr3_pr2 c (THead (Flat Appl) t0 u2) (THead (Flat Appl) x1
688 u2) (pr2_head_1 c t0 x1 H15 (Flat Appl) u2)))))))) H33))) x3 H28))) x4
689 H27))))) H26))) (\lambda (H25: (((eq T (THead (Flat Appl) x x0) (THead (Flat
690 Appl) x3 x4)) \to (\forall (P: Prop).P)))).(H8 (THead (Flat Appl) x3 x4) H25
691 (pr3_flat c x x3 (pr3_pr2 c x x3 H21) x0 x4 (pr3_pr2 c x0 x4 H22) Appl) x3 x4
692 (refl_equal T (THead (Flat Appl) x3 x4)) x1 (sn3_pr3_trans c t0 (sn3_sing c
693 t0 H5) x1 (pr3_pr2 c t0 x1 H15)) (\lambda (u2: T).(\lambda (H26: (pr3 c
694 (THead (Flat Appl) x3 x4) u2)).(\lambda (H27: (((iso (THead (Flat Appl) x3
695 x4) u2) \to (\forall (P: Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t0
696 u2) (H7 u2 (pr3_sing c (THead (Flat Appl) x x4) (THead (Flat Appl) x x0)
697 (pr2_thin_dx c x0 x4 H22 x Appl) u2 (pr3_sing c (THead (Flat Appl) x3 x4)
698 (THead (Flat Appl) x x4) (pr2_head_1 c x x3 H21 (Flat Appl) x4) u2 H26))
699 (\lambda (H28: (iso (THead (Flat Appl) x x0) u2)).(\lambda (P: Prop).(H27
700 (iso_trans (THead (Flat Appl) x3 x4) (THead (Flat Appl) x x0) (iso_head x3 x
701 x4 x0 (Flat Appl)) u2 H28) P)))) (THead (Flat Appl) x1 u2) (pr3_pr2 c (THead
702 (Flat Appl) t0 u2) (THead (Flat Appl) x1 u2) (pr2_head_1 c t0 x1 H15 (Flat
703 Appl) u2)))))))) H24))) x2 H20))))))) H19)) (\lambda (H19: (ex4_4 T T T T
704 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T x0
705 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
706 T).(\lambda (t4: T).(eq T x2 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
707 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
708 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b:
709 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4))))))))).(ex4_4_ind T T T
710 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T x0
711 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
712 T).(\lambda (t4: T).(eq T x2 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
713 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
714 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b:
715 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4))))))) (sn3 c (THead (Flat
716 Appl) x1 x2)) (\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda
717 (x6: T).(\lambda (H20: (eq T x0 (THead (Bind Abst) x3 x4))).(\lambda (H21:
718 (eq T x2 (THead (Bind Abbr) x5 x6))).(\lambda (H22: (pr2 c x x5)).(\lambda
719 (H23: ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x4
720 x6))))).(let H24 \def (eq_ind T x2 (\lambda (t: T).((eq T (THead (Flat Appl)
721 t0 (THead (Flat Appl) x x0)) (THead (Flat Appl) x1 t)) \to (\forall (P:
722 Prop).P))) H17 (THead (Bind Abbr) x5 x6) H21) in (eq_ind_r T (THead (Bind
723 Abbr) x5 x6) (\lambda (t: T).(sn3 c (THead (Flat Appl) x1 t))) (let H25 \def
724 (eq_ind T x0 (\lambda (t: T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl)
725 x t)) (THead (Flat Appl) x1 (THead (Bind Abbr) x5 x6))) \to (\forall (P:
726 Prop).P))) H24 (THead (Bind Abst) x3 x4) H20) in (let H26 \def (eq_ind T x0
727 (\lambda (t: T).(\forall (t4: T).((((eq T (THead (Flat Appl) x t) t4) \to
728 (\forall (P: Prop).P))) \to ((pr3 c (THead (Flat Appl) x t) t4) \to (sn3 c
729 t4))))) H9 (THead (Bind Abst) x3 x4) H20) in (let H27 \def (eq_ind T x0
730 (\lambda (t: T).(\forall (t4: T).((((eq T (THead (Flat Appl) x t) t4) \to
731 (\forall (P: Prop).P))) \to ((pr3 c (THead (Flat Appl) x t) t4) \to (\forall
732 (x7: T).(\forall (x8: T).((eq T t4 (THead (Flat Appl) x7 x8)) \to (\forall
733 (v3: T).((sn3 c v3) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x7 x8)
734 u2) \to ((((iso (THead (Flat Appl) x7 x8) u2) \to (\forall (P: Prop).P))) \to
735 (sn3 c (THead (Flat Appl) v3 u2)))))) \to (sn3 c (THead (Flat Appl) v3 (THead
736 (Flat Appl) x7 x8))))))))))))) H8 (THead (Bind Abst) x3 x4) H20) in (let H28
737 \def (eq_ind T x0 (\lambda (t: T).(\forall (u2: T).((pr3 c (THead (Flat Appl)
738 x t) u2) \to ((((iso (THead (Flat Appl) x t) u2) \to (\forall (P: Prop).P)))
739 \to (sn3 c (THead (Flat Appl) t0 u2)))))) H7 (THead (Bind Abst) x3 x4) H20)
740 in (let H29 \def (eq_ind T x0 (\lambda (t: T).(\forall (t4: T).((((eq T t0
741 t4) \to (\forall (P: Prop).P))) \to ((pr3 c t0 t4) \to (((\forall (u2:
742 T).((pr3 c (THead (Flat Appl) x t) u2) \to ((((iso (THead (Flat Appl) x t)
743 u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) t4 u2)))))) \to
744 (sn3 c (THead (Flat Appl) t4 (THead (Flat Appl) x t)))))))) H6 (THead (Bind
745 Abst) x3 x4) H20) in (sn3_pr3_trans c (THead (Flat Appl) t0 (THead (Bind
746 Abbr) x5 x6)) (H28 (THead (Bind Abbr) x5 x6) (pr3_sing c (THead (Bind Abbr) x
747 x4) (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) (pr2_free c (THead (Flat
748 Appl) x (THead (Bind Abst) x3 x4)) (THead (Bind Abbr) x x4) (pr0_beta x3 x x
749 (pr0_refl x) x4 x4 (pr0_refl x4))) (THead (Bind Abbr) x5 x6) (pr3_head_12 c x
750 x5 (pr3_pr2 c x x5 H22) (Bind Abbr) x4 x6 (pr3_pr2 (CHead c (Bind Abbr) x5)
751 x4 x6 (H23 Abbr x5)))) (\lambda (H30: (iso (THead (Flat Appl) x (THead (Bind
752 Abst) x3 x4)) (THead (Bind Abbr) x5 x6))).(\lambda (P: Prop).(let H31 \def
753 (match H30 in iso return (\lambda (t: T).(\lambda (t4: T).(\lambda (_: (iso t
754 t4)).((eq T t (THead (Flat Appl) x (THead (Bind Abst) x3 x4))) \to ((eq T t4
755 (THead (Bind Abbr) x5 x6)) \to P))))) with [(iso_sort n1 n2) \Rightarrow
756 (\lambda (H31: (eq T (TSort n1) (THead (Flat Appl) x (THead (Bind Abst) x3
757 x4)))).(\lambda (H32: (eq T (TSort n2) (THead (Bind Abbr) x5 x6))).((let H33
758 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_:
759 T).Prop) with [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False |
760 (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) x (THead (Bind Abst)
761 x3 x4)) H31) in (False_ind ((eq T (TSort n2) (THead (Bind Abbr) x5 x6)) \to
762 P) H33)) H32))) | (iso_lref i1 i2) \Rightarrow (\lambda (H31: (eq T (TLRef
763 i1) (THead (Flat Appl) x (THead (Bind Abst) x3 x4)))).(\lambda (H32: (eq T
764 (TLRef i2) (THead (Bind Abbr) x5 x6))).((let H33 \def (eq_ind T (TLRef i1)
765 (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with [(TSort _)
766 \Rightarrow False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow
767 False])) I (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) H31) in (False_ind
768 ((eq T (TLRef i2) (THead (Bind Abbr) x5 x6)) \to P) H33)) H32))) | (iso_head
769 v4 v5 t4 t5 k) \Rightarrow (\lambda (H31: (eq T (THead k v4 t4) (THead (Flat
770 Appl) x (THead (Bind Abst) x3 x4)))).(\lambda (H32: (eq T (THead k v5 t5)
771 (THead (Bind Abbr) x5 x6))).((let H33 \def (f_equal T T (\lambda (e:
772 T).(match e in T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t4 |
773 (TLRef _) \Rightarrow t4 | (THead _ _ t) \Rightarrow t])) (THead k v4 t4)
774 (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) H31) in ((let H34 \def
775 (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T) with
776 [(TSort _) \Rightarrow v4 | (TLRef _) \Rightarrow v4 | (THead _ t _)
777 \Rightarrow t])) (THead k v4 t4) (THead (Flat Appl) x (THead (Bind Abst) x3
778 x4)) H31) in ((let H35 \def (f_equal T K (\lambda (e: T).(match e in T return
779 (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k |
780 (THead k0 _ _) \Rightarrow k0])) (THead k v4 t4) (THead (Flat Appl) x (THead
781 (Bind Abst) x3 x4)) H31) in (eq_ind K (Flat Appl) (\lambda (k0: K).((eq T v4
782 x) \to ((eq T t4 (THead (Bind Abst) x3 x4)) \to ((eq T (THead k0 v5 t5)
783 (THead (Bind Abbr) x5 x6)) \to P)))) (\lambda (H36: (eq T v4 x)).(eq_ind T x
784 (\lambda (_: T).((eq T t4 (THead (Bind Abst) x3 x4)) \to ((eq T (THead (Flat
785 Appl) v5 t5) (THead (Bind Abbr) x5 x6)) \to P))) (\lambda (H37: (eq T t4
786 (THead (Bind Abst) x3 x4))).(eq_ind T (THead (Bind Abst) x3 x4) (\lambda (_:
787 T).((eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6)) \to P))
788 (\lambda (H38: (eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5
789 x6))).(let H39 \def (eq_ind T (THead (Flat Appl) v5 t5) (\lambda (e:
790 T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
791 False | (TLRef _) \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in
792 K return (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _)
793 \Rightarrow True])])) I (THead (Bind Abbr) x5 x6) H38) in (False_ind P H39)))
794 t4 (sym_eq T t4 (THead (Bind Abst) x3 x4) H37))) v4 (sym_eq T v4 x H36))) k
795 (sym_eq K k (Flat Appl) H35))) H34)) H33)) H32)))]) in (H31 (refl_equal T
796 (THead (Flat Appl) x (THead (Bind Abst) x3 x4))) (refl_equal T (THead (Bind
797 Abbr) x5 x6))))))) (THead (Flat Appl) x1 (THead (Bind Abbr) x5 x6)) (pr3_pr2
798 c (THead (Flat Appl) t0 (THead (Bind Abbr) x5 x6)) (THead (Flat Appl) x1
799 (THead (Bind Abbr) x5 x6)) (pr2_head_1 c t0 x1 H15 (Flat Appl) (THead (Bind
800 Abbr) x5 x6))))))))) x2 H21)))))))))) H19)) (\lambda (H19: (ex6_6 B T T T T T
801 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
802 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
803 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T x0
804 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
805 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T x2 (THead (Bind
806 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
807 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
808 (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
809 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
810 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
811 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))))).(ex6_6_ind
812 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
813 T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
814 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
815 (_: T).(eq T x0 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
816 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
817 x2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
818 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
819 T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1:
820 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
821 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
822 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))
823 (sn3 c (THead (Flat Appl) x1 x2)) (\lambda (x3: B).(\lambda (x4: T).(\lambda
824 (x5: T).(\lambda (x6: T).(\lambda (x7: T).(\lambda (x8: T).(\lambda (H20:
825 (not (eq B x3 Abst))).(\lambda (H21: (eq T x0 (THead (Bind x3) x4
826 x5))).(\lambda (H22: (eq T x2 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S
827 O) O x7) x6)))).(\lambda (H23: (pr2 c x x7)).(\lambda (H24: (pr2 c x4
828 x8)).(\lambda (H25: (pr2 (CHead c (Bind x3) x8) x5 x6)).(let H26 \def (eq_ind
829 T x2 (\lambda (t: T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0))
830 (THead (Flat Appl) x1 t)) \to (\forall (P: Prop).P))) H17 (THead (Bind x3) x8
831 (THead (Flat Appl) (lift (S O) O x7) x6)) H22) in (eq_ind_r T (THead (Bind
832 x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)) (\lambda (t: T).(sn3 c
833 (THead (Flat Appl) x1 t))) (let H27 \def (eq_ind T x0 (\lambda (t: T).((eq T
834 (THead (Flat Appl) t0 (THead (Flat Appl) x t)) (THead (Flat Appl) x1 (THead
835 (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)))) \to (\forall (P:
836 Prop).P))) H26 (THead (Bind x3) x4 x5) H21) in (let H28 \def (eq_ind T x0
837 (\lambda (t: T).(\forall (t4: T).((((eq T (THead (Flat Appl) x t) t4) \to
838 (\forall (P: Prop).P))) \to ((pr3 c (THead (Flat Appl) x t) t4) \to (sn3 c
839 t4))))) H9 (THead (Bind x3) x4 x5) H21) in (let H29 \def (eq_ind T x0
840 (\lambda (t: T).(\forall (t4: T).((((eq T (THead (Flat Appl) x t) t4) \to
841 (\forall (P: Prop).P))) \to ((pr3 c (THead (Flat Appl) x t) t4) \to (\forall
842 (x9: T).(\forall (x10: T).((eq T t4 (THead (Flat Appl) x9 x10)) \to (\forall
843 (v3: T).((sn3 c v3) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x9 x10)
844 u2) \to ((((iso (THead (Flat Appl) x9 x10) u2) \to (\forall (P: Prop).P)))
845 \to (sn3 c (THead (Flat Appl) v3 u2)))))) \to (sn3 c (THead (Flat Appl) v3
846 (THead (Flat Appl) x9 x10))))))))))))) H8 (THead (Bind x3) x4 x5) H21) in
847 (let H30 \def (eq_ind T x0 (\lambda (t: T).(\forall (u2: T).((pr3 c (THead
848 (Flat Appl) x t) u2) \to ((((iso (THead (Flat Appl) x t) u2) \to (\forall (P:
849 Prop).P))) \to (sn3 c (THead (Flat Appl) t0 u2)))))) H7 (THead (Bind x3) x4
850 x5) H21) in (let H31 \def (eq_ind T x0 (\lambda (t: T).(\forall (t4:
851 T).((((eq T t0 t4) \to (\forall (P: Prop).P))) \to ((pr3 c t0 t4) \to
852 (((\forall (u2: T).((pr3 c (THead (Flat Appl) x t) u2) \to ((((iso (THead
853 (Flat Appl) x t) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat
854 Appl) t4 u2)))))) \to (sn3 c (THead (Flat Appl) t4 (THead (Flat Appl) x
855 t)))))))) H6 (THead (Bind x3) x4 x5) H21) in (sn3_pr3_trans c (THead (Flat
856 Appl) t0 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) (H30
857 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)) (pr3_sing c
858 (THead (Bind x3) x4 (THead (Flat Appl) (lift (S O) O x) x5)) (THead (Flat
859 Appl) x (THead (Bind x3) x4 x5)) (pr2_free c (THead (Flat Appl) x (THead
860 (Bind x3) x4 x5)) (THead (Bind x3) x4 (THead (Flat Appl) (lift (S O) O x)
861 x5)) (pr0_upsilon x3 H20 x x (pr0_refl x) x4 x4 (pr0_refl x4) x5 x5 (pr0_refl
862 x5))) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
863 (pr3_head_12 c x4 x8 (pr3_pr2 c x4 x8 H24) (Bind x3) (THead (Flat Appl) (lift
864 (S O) O x) x5) (THead (Flat Appl) (lift (S O) O x7) x6) (pr3_head_12 (CHead c
865 (Bind x3) x8) (lift (S O) O x) (lift (S O) O x7) (pr3_lift (CHead c (Bind x3)
866 x8) c (S O) O (drop_drop (Bind x3) O c c (drop_refl c) x8) x x7 (pr3_pr2 c x
867 x7 H23)) (Flat Appl) x5 x6 (pr3_pr2 (CHead (CHead c (Bind x3) x8) (Flat Appl)
868 (lift (S O) O x7)) x5 x6 (pr2_cflat (CHead c (Bind x3) x8) x5 x6 H25 Appl
869 (lift (S O) O x7)))))) (\lambda (H32: (iso (THead (Flat Appl) x (THead (Bind
870 x3) x4 x5)) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7)
871 x6)))).(\lambda (P: Prop).(let H33 \def (match H32 in iso return (\lambda (t:
872 T).(\lambda (t4: T).(\lambda (_: (iso t t4)).((eq T t (THead (Flat Appl) x
873 (THead (Bind x3) x4 x5))) \to ((eq T t4 (THead (Bind x3) x8 (THead (Flat
874 Appl) (lift (S O) O x7) x6))) \to P))))) with [(iso_sort n1 n2) \Rightarrow
875 (\lambda (H33: (eq T (TSort n1) (THead (Flat Appl) x (THead (Bind x3) x4
876 x5)))).(\lambda (H34: (eq T (TSort n2) (THead (Bind x3) x8 (THead (Flat Appl)
877 (lift (S O) O x7) x6)))).((let H35 \def (eq_ind T (TSort n1) (\lambda (e:
878 T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
879 True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I
880 (THead (Flat Appl) x (THead (Bind x3) x4 x5)) H33) in (False_ind ((eq T
881 (TSort n2) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to
882 P) H35)) H34))) | (iso_lref i1 i2) \Rightarrow (\lambda (H33: (eq T (TLRef
883 i1) (THead (Flat Appl) x (THead (Bind x3) x4 x5)))).(\lambda (H34: (eq T
884 (TLRef i2) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7)
885 x6)))).((let H35 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T
886 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
887 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) x
888 (THead (Bind x3) x4 x5)) H33) in (False_ind ((eq T (TLRef i2) (THead (Bind
889 x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to P) H35)) H34))) |
890 (iso_head v4 v5 t4 t5 k) \Rightarrow (\lambda (H33: (eq T (THead k v4 t4)
891 (THead (Flat Appl) x (THead (Bind x3) x4 x5)))).(\lambda (H34: (eq T (THead k
892 v5 t5) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)))).((let
893 H35 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
894 with [(TSort _) \Rightarrow t4 | (TLRef _) \Rightarrow t4 | (THead _ _ t)
895 \Rightarrow t])) (THead k v4 t4) (THead (Flat Appl) x (THead (Bind x3) x4
896 x5)) H33) in ((let H36 \def (f_equal T T (\lambda (e: T).(match e in T return
897 (\lambda (_: T).T) with [(TSort _) \Rightarrow v4 | (TLRef _) \Rightarrow v4
898 | (THead _ t _) \Rightarrow t])) (THead k v4 t4) (THead (Flat Appl) x (THead
899 (Bind x3) x4 x5)) H33) in ((let H37 \def (f_equal T K (\lambda (e: T).(match
900 e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _)
901 \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k v4 t4) (THead (Flat
902 Appl) x (THead (Bind x3) x4 x5)) H33) in (eq_ind K (Flat Appl) (\lambda (k0:
903 K).((eq T v4 x) \to ((eq T t4 (THead (Bind x3) x4 x5)) \to ((eq T (THead k0
904 v5 t5) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to
905 P)))) (\lambda (H38: (eq T v4 x)).(eq_ind T x (\lambda (_: T).((eq T t4
906 (THead (Bind x3) x4 x5)) \to ((eq T (THead (Flat Appl) v5 t5) (THead (Bind
907 x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to P))) (\lambda (H39: (eq
908 T t4 (THead (Bind x3) x4 x5))).(eq_ind T (THead (Bind x3) x4 x5) (\lambda (_:
909 T).((eq T (THead (Flat Appl) v5 t5) (THead (Bind x3) x8 (THead (Flat Appl)
910 (lift (S O) O x7) x6))) \to P)) (\lambda (H40: (eq T (THead (Flat Appl) v5
911 t5) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)))).(let H41
912 \def (eq_ind T (THead (Flat Appl) v5 t5) (\lambda (e: T).(match e in T return
913 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
914 \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in K return (\lambda
915 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
916 True])])) I (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
917 H40) in (False_ind P H41))) t4 (sym_eq T t4 (THead (Bind x3) x4 x5) H39))) v4
918 (sym_eq T v4 x H38))) k (sym_eq K k (Flat Appl) H37))) H36)) H35)) H34)))])
919 in (H33 (refl_equal T (THead (Flat Appl) x (THead (Bind x3) x4 x5)))
920 (refl_equal T (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7)
921 x6)))))))) (THead (Flat Appl) x1 (THead (Bind x3) x8 (THead (Flat Appl) (lift
922 (S O) O x7) x6))) (pr3_pr2 c (THead (Flat Appl) t0 (THead (Bind x3) x8 (THead
923 (Flat Appl) (lift (S O) O x7) x6))) (THead (Flat Appl) x1 (THead (Bind x3) x8
924 (THead (Flat Appl) (lift (S O) O x7) x6))) (pr2_head_1 c t0 x1 H15 (Flat
925 Appl) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))))))))))
926 x2 H22)))))))))))))) H19)) H18)) t3 H14))))))) H13)) (\lambda (H13: (ex4_4 T
927 T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
928 (THead (Flat Appl) x x0) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
929 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind
930 Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
931 (_: T).(pr2 c t0 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
932 T).(\lambda (t4: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
933 z1 t4))))))))).(ex4_4_ind T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
934 (_: T).(\lambda (_: T).(eq T (THead (Flat Appl) x x0) (THead (Bind Abst) y1
935 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t4:
936 T).(eq T t3 (THead (Bind Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_:
937 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2))))) (\lambda (_:
938 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b: B).(\forall
939 (u: T).(pr2 (CHead c (Bind b) u) z1 t4))))))) (sn3 c t3) (\lambda (x1:
940 T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda (H14: (eq T
941 (THead (Flat Appl) x x0) (THead (Bind Abst) x1 x2))).(\lambda (H15: (eq T t3
942 (THead (Bind Abbr) x3 x4))).(\lambda (_: (pr2 c t0 x3)).(\lambda (_:
943 ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x2 x4))))).(let
944 H18 \def (eq_ind T t3 (\lambda (t: T).((eq T (THead (Flat Appl) t0 (THead
945 (Flat Appl) x x0)) t) \to (\forall (P: Prop).P))) H10 (THead (Bind Abbr) x3
946 x4) H15) in (eq_ind_r T (THead (Bind Abbr) x3 x4) (\lambda (t: T).(sn3 c t))
947 (let H19 \def (eq_ind T (THead (Flat Appl) x x0) (\lambda (ee: T).(match ee
948 in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef
949 _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return
950 (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
951 True])])) I (THead (Bind Abst) x1 x2) H14) in (False_ind (sn3 c (THead (Bind
952 Abbr) x3 x4)) H19)) t3 H15)))))))))) H13)) (\lambda (H13: (ex6_6 B T T T T T
953 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
954 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
955 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T
956 (THead (Flat Appl) x x0) (THead (Bind b) y1 z1)))))))) (\lambda (b:
957 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
958 (y2: T).(eq T t3 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2)
959 z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
960 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2))))))) (\lambda (_:
961 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
962 (y2: T).(pr2 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
963 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b)
964 y2) z1 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_:
965 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
966 b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
967 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Appl) x x0) (THead
968 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
969 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t3 (THead (Bind
970 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
971 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
972 (_: T).(pr2 c t0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
973 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
974 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
975 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))) (sn3 c t3)
976 (\lambda (x1: B).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda
977 (x5: T).(\lambda (x6: T).(\lambda (_: (not (eq B x1 Abst))).(\lambda (H15:
978 (eq T (THead (Flat Appl) x x0) (THead (Bind x1) x2 x3))).(\lambda (H16: (eq T
979 t3 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4)))).(\lambda
980 (_: (pr2 c t0 x5)).(\lambda (_: (pr2 c x2 x6)).(\lambda (_: (pr2 (CHead c
981 (Bind x1) x6) x3 x4)).(let H20 \def (eq_ind T t3 (\lambda (t: T).((eq T
982 (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t) \to (\forall (P:
983 Prop).P))) H10 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
984 H16) in (eq_ind_r T (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5)
985 x4)) (\lambda (t: T).(sn3 c t)) (let H21 \def (eq_ind T (THead (Flat Appl) x
986 x0) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
987 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
988 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
989 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind x1) x2 x3)
990 H15) in (False_ind (sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O)
991 O x5) x4))) H21)) t3 H16)))))))))))))) H13)) H12)))))))))))) v2 H4))))))))) y
994 theorem sn3_appl_appls:
995 \forall (v1: T).(\forall (t1: T).(\forall (vs: TList).(let u1 \def (THeads
996 (Flat Appl) (TCons v1 vs) t1) in (\forall (c: C).((sn3 c u1) \to (\forall
997 (v2: T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2)
998 \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to
999 (sn3 c (THead (Flat Appl) v2 u1))))))))))
1001 \lambda (v1: T).(\lambda (t1: T).(\lambda (vs: TList).(let u1 \def (THeads
1002 (Flat Appl) (TCons v1 vs) t1) in (\lambda (c: C).(\lambda (H: (sn3 c (THead
1003 (Flat Appl) v1 (THeads (Flat Appl) vs t1)))).(\lambda (v2: T).(\lambda (H0:
1004 (sn3 c v2)).(\lambda (H1: ((\forall (u2: T).((pr3 c (THead (Flat Appl) v1
1005 (THeads (Flat Appl) vs t1)) u2) \to ((((iso (THead (Flat Appl) v1 (THeads
1006 (Flat Appl) vs t1)) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat
1007 Appl) v2 u2))))))).(sn3_appl_appl v1 (THeads (Flat Appl) vs t1) c H v2 H0
1010 theorem sn3_appls_lref:
1011 \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (us:
1012 TList).((sns3 c us) \to (sn3 c (THeads (Flat Appl) us (TLRef i)))))))
1014 \lambda (c: C).(\lambda (i: nat).(\lambda (H: (nf2 c (TLRef i))).(\lambda
1015 (us: TList).(TList_ind (\lambda (t: TList).((sns3 c t) \to (sn3 c (THeads
1016 (Flat Appl) t (TLRef i))))) (\lambda (_: True).(sn3_nf2 c (TLRef i) H))
1017 (\lambda (t: T).(\lambda (t0: TList).(TList_ind (\lambda (t1: TList).((((sns3
1018 c t1) \to (sn3 c (THeads (Flat Appl) t1 (TLRef i))))) \to ((land (sn3 c t)
1019 (sns3 c t1)) \to (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t1 (TLRef
1020 i))))))) (\lambda (_: (((sns3 c TNil) \to (sn3 c (THeads (Flat Appl) TNil
1021 (TLRef i)))))).(\lambda (H1: (land (sn3 c t) (sns3 c TNil))).(let H2 \def H1
1022 in (and_ind (sn3 c t) True (sn3 c (THead (Flat Appl) t (THeads (Flat Appl)
1023 TNil (TLRef i)))) (\lambda (H3: (sn3 c t)).(\lambda (_: True).(sn3_appl_lref
1024 c i H t H3))) H2)))) (\lambda (t1: T).(\lambda (t2: TList).(\lambda (_:
1025 (((((sns3 c t2) \to (sn3 c (THeads (Flat Appl) t2 (TLRef i))))) \to ((land
1026 (sn3 c t) (sns3 c t2)) \to (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t2
1027 (TLRef i)))))))).(\lambda (H1: (((sns3 c (TCons t1 t2)) \to (sn3 c (THeads
1028 (Flat Appl) (TCons t1 t2) (TLRef i)))))).(\lambda (H2: (land (sn3 c t) (sns3
1029 c (TCons t1 t2)))).(let H3 \def H2 in (and_ind (sn3 c t) (land (sn3 c t1)
1030 (sns3 c t2)) (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2)
1031 (TLRef i)))) (\lambda (H4: (sn3 c t)).(\lambda (H5: (land (sn3 c t1) (sns3 c
1032 t2))).(and_ind (sn3 c t1) (sns3 c t2) (sn3 c (THead (Flat Appl) t (THeads
1033 (Flat Appl) (TCons t1 t2) (TLRef i)))) (\lambda (H6: (sn3 c t1)).(\lambda
1034 (H7: (sns3 c t2)).(sn3_appl_appls t1 (TLRef i) t2 c (H1 (conj (sn3 c t1)
1035 (sns3 c t2) H6 H7)) t H4 (\lambda (u2: T).(\lambda (H8: (pr3 c (THeads (Flat
1036 Appl) (TCons t1 t2) (TLRef i)) u2)).(\lambda (H9: (((iso (THeads (Flat Appl)
1037 (TCons t1 t2) (TLRef i)) u2) \to (\forall (P: Prop).P)))).(H9
1038 (nf2_iso_appls_lref c i H (TCons t1 t2) u2 H8) (sn3 c (THead (Flat Appl) t
1039 u2))))))))) H5))) H3))))))) t0))) us)))).
1041 theorem sn3_appls_cast:
1042 \forall (c: C).(\forall (vs: TList).(\forall (u: T).((sn3 c (THeads (Flat
1043 Appl) vs u)) \to (\forall (t: T).((sn3 c (THeads (Flat Appl) vs t)) \to (sn3
1044 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))))))))
1046 \lambda (c: C).(\lambda (vs: TList).(TList_ind (\lambda (t: TList).(\forall
1047 (u: T).((sn3 c (THeads (Flat Appl) t u)) \to (\forall (t0: T).((sn3 c (THeads
1048 (Flat Appl) t t0)) \to (sn3 c (THeads (Flat Appl) t (THead (Flat Cast) u
1049 t0)))))))) (\lambda (u: T).(\lambda (H: (sn3 c u)).(\lambda (t: T).(\lambda
1050 (H0: (sn3 c t)).(sn3_cast c u H t H0))))) (\lambda (t: T).(\lambda (t0:
1051 TList).(TList_ind (\lambda (t1: TList).(((\forall (u: T).((sn3 c (THeads
1052 (Flat Appl) t1 u)) \to (\forall (t2: T).((sn3 c (THeads (Flat Appl) t1 t2))
1053 \to (sn3 c (THeads (Flat Appl) t1 (THead (Flat Cast) u t2)))))))) \to
1054 (\forall (u: T).((sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t1 u))) \to
1055 (\forall (t2: T).((sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t1 t2)))
1056 \to (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t1 (THead (Flat Cast) u
1057 t2)))))))))) (\lambda (_: ((\forall (u: T).((sn3 c (THeads (Flat Appl) TNil
1058 u)) \to (\forall (t1: T).((sn3 c (THeads (Flat Appl) TNil t1)) \to (sn3 c
1059 (THeads (Flat Appl) TNil (THead (Flat Cast) u t1))))))))).(\lambda (u:
1060 T).(\lambda (H0: (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) TNil
1061 u)))).(\lambda (t1: T).(\lambda (H1: (sn3 c (THead (Flat Appl) t (THeads
1062 (Flat Appl) TNil t1)))).(sn3_appl_cast c t u H0 t1 H1)))))) (\lambda (t1:
1063 T).(\lambda (t2: TList).(\lambda (_: ((((\forall (u: T).((sn3 c (THeads (Flat
1064 Appl) t2 u)) \to (\forall (t3: T).((sn3 c (THeads (Flat Appl) t2 t3)) \to
1065 (sn3 c (THeads (Flat Appl) t2 (THead (Flat Cast) u t3)))))))) \to (\forall
1066 (u: T).((sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t2 u))) \to (\forall
1067 (t3: T).((sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t2 t3))) \to (sn3 c
1068 (THead (Flat Appl) t (THeads (Flat Appl) t2 (THead (Flat Cast) u
1069 t3))))))))))).(\lambda (H0: ((\forall (u: T).((sn3 c (THeads (Flat Appl)
1070 (TCons t1 t2) u)) \to (\forall (t3: T).((sn3 c (THeads (Flat Appl) (TCons t1
1071 t2) t3)) \to (sn3 c (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u
1072 t3))))))))).(\lambda (u: T).(\lambda (H1: (sn3 c (THead (Flat Appl) t (THeads
1073 (Flat Appl) (TCons t1 t2) u)))).(\lambda (t3: T).(\lambda (H2: (sn3 c (THead
1074 (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) t3)))).(let H_x \def
1075 (sn3_gen_flat Appl c t (THeads (Flat Appl) (TCons t1 t2) t3) H2) in (let H3
1076 \def H_x in (and_ind (sn3 c t) (sn3 c (THeads (Flat Appl) (TCons t1 t2) t3))
1077 (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) (THead (Flat
1078 Cast) u t3)))) (\lambda (_: (sn3 c t)).(\lambda (H5: (sn3 c (THeads (Flat
1079 Appl) (TCons t1 t2) t3))).(let H6 \def H5 in (let H_x0 \def (sn3_gen_flat
1080 Appl c t (THeads (Flat Appl) (TCons t1 t2) u) H1) in (let H7 \def H_x0 in
1081 (and_ind (sn3 c t) (sn3 c (THeads (Flat Appl) (TCons t1 t2) u)) (sn3 c (THead
1082 (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3))))
1083 (\lambda (H8: (sn3 c t)).(\lambda (H9: (sn3 c (THeads (Flat Appl) (TCons t1
1084 t2) u))).(let H10 \def H9 in (sn3_appl_appls t1 (THead (Flat Cast) u t3) t2 c
1085 (H0 u H10 t3 H6) t H8 (\lambda (u2: T).(\lambda (H11: (pr3 c (THeads (Flat
1086 Appl) (TCons t1 t2) (THead (Flat Cast) u t3)) u2)).(\lambda (H12: (((iso
1087 (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)) u2) \to (\forall
1088 (P: Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t (THeads (Flat Appl)
1089 (TCons t1 t2) t3)) H2 (THead (Flat Appl) t u2) (pr3_thin_dx c (THeads (Flat
1090 Appl) (TCons t1 t2) t3) u2 (pr3_iso_appls_cast c u t3 (TCons t1 t2) u2 H11
1091 H12) t Appl))))))))) H7)))))) H3))))))))))) t0))) vs)).
1094 \forall (d: C).(\forall (t: T).((sn3 d t) \to (\forall (c: C).(\forall (h:
1095 nat).(\forall (i: nat).((drop h i c d) \to (sn3 c (lift h i t))))))))
1097 \lambda (d: C).(\lambda (t: T).(\lambda (H: (sn3 d t)).(sn3_ind d (\lambda
1098 (t0: T).(\forall (c: C).(\forall (h: nat).(\forall (i: nat).((drop h i c d)
1099 \to (sn3 c (lift h i t0))))))) (\lambda (t1: T).(\lambda (_: ((\forall (t2:
1100 T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 d t1 t2) \to (sn3 d
1101 t2)))))).(\lambda (H1: ((\forall (t2: T).((((eq T t1 t2) \to (\forall (P:
1102 Prop).P))) \to ((pr3 d t1 t2) \to (\forall (c: C).(\forall (h: nat).(\forall
1103 (i: nat).((drop h i c d) \to (sn3 c (lift h i t2))))))))))).(\lambda (c:
1104 C).(\lambda (h: nat).(\lambda (i: nat).(\lambda (H2: (drop h i c
1105 d)).(sn3_pr2_intro c (lift h i t1) (\lambda (t2: T).(\lambda (H3: (((eq T
1106 (lift h i t1) t2) \to (\forall (P: Prop).P)))).(\lambda (H4: (pr2 c (lift h i
1107 t1) t2)).(let H5 \def (pr2_gen_lift c t1 t2 h i H4 d H2) in (ex2_ind T
1108 (\lambda (t3: T).(eq T t2 (lift h i t3))) (\lambda (t3: T).(pr2 d t1 t3))
1109 (sn3 c t2) (\lambda (x: T).(\lambda (H6: (eq T t2 (lift h i x))).(\lambda
1110 (H7: (pr2 d t1 x)).(let H8 \def (eq_ind T t2 (\lambda (t0: T).((eq T (lift h
1111 i t1) t0) \to (\forall (P: Prop).P))) H3 (lift h i x) H6) in (eq_ind_r T
1112 (lift h i x) (\lambda (t0: T).(sn3 c t0)) (H1 x (\lambda (H9: (eq T t1
1113 x)).(\lambda (P: Prop).(let H10 \def (eq_ind_r T x (\lambda (t0: T).((eq T
1114 (lift h i t1) (lift h i t0)) \to (\forall (P0: Prop).P0))) H8 t1 H9) in (let
1115 H11 \def (eq_ind_r T x (\lambda (t0: T).(pr2 d t1 t0)) H7 t1 H9) in (H10
1116 (refl_equal T (lift h i t1)) P))))) (pr3_pr2 d t1 x H7) c h i H2) t2 H6)))))
1117 H5))))))))))))) t H))).
1120 \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
1121 (CHead d (Bind Abbr) v)) \to ((sn3 d v) \to (sn3 c (TLRef i)))))))
1123 \lambda (c: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda
1124 (H: (getl i c (CHead d (Bind Abbr) v))).(\lambda (H0: (sn3 d
1125 v)).(sn3_pr2_intro c (TLRef i) (\lambda (t2: T).(\lambda (H1: (((eq T (TLRef
1126 i) t2) \to (\forall (P: Prop).P)))).(\lambda (H2: (pr2 c (TLRef i) t2)).(let
1127 H3 \def (pr2_gen_lref c t2 i H2) in (or_ind (eq T t2 (TLRef i)) (ex2_2 C T
1128 (\lambda (d0: C).(\lambda (u: T).(getl i c (CHead d0 (Bind Abbr) u))))
1129 (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift (S i) O u))))) (sn3 c t2)
1130 (\lambda (H4: (eq T t2 (TLRef i))).(let H5 \def (eq_ind T t2 (\lambda (t:
1131 T).((eq T (TLRef i) t) \to (\forall (P: Prop).P))) H1 (TLRef i) H4) in
1132 (eq_ind_r T (TLRef i) (\lambda (t: T).(sn3 c t)) (H5 (refl_equal T (TLRef i))
1133 (sn3 c (TLRef i))) t2 H4))) (\lambda (H4: (ex2_2 C T (\lambda (d0:
1134 C).(\lambda (u: T).(getl i c (CHead d0 (Bind Abbr) u)))) (\lambda (_:
1135 C).(\lambda (u: T).(eq T t2 (lift (S i) O u)))))).(ex2_2_ind C T (\lambda
1136 (d0: C).(\lambda (u: T).(getl i c (CHead d0 (Bind Abbr) u)))) (\lambda (_:
1137 C).(\lambda (u: T).(eq T t2 (lift (S i) O u)))) (sn3 c t2) (\lambda (x0:
1138 C).(\lambda (x1: T).(\lambda (H5: (getl i c (CHead x0 (Bind Abbr)
1139 x1))).(\lambda (H6: (eq T t2 (lift (S i) O x1))).(let H7 \def (eq_ind T t2
1140 (\lambda (t: T).((eq T (TLRef i) t) \to (\forall (P: Prop).P))) H1 (lift (S
1141 i) O x1) H6) in (eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(sn3 c t)) (let
1142 H8 \def (eq_ind C (CHead d (Bind Abbr) v) (\lambda (c0: C).(getl i c c0)) H
1143 (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead d (Bind Abbr) v) i H (CHead x0
1144 (Bind Abbr) x1) H5)) in (let H9 \def (f_equal C C (\lambda (e: C).(match e in
1145 C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d | (CHead c0 _ _)
1146 \Rightarrow c0])) (CHead d (Bind Abbr) v) (CHead x0 (Bind Abbr) x1)
1147 (getl_mono c (CHead d (Bind Abbr) v) i H (CHead x0 (Bind Abbr) x1) H5)) in
1148 ((let H10 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
1149 C).T) with [(CSort _) \Rightarrow v | (CHead _ _ t) \Rightarrow t])) (CHead d
1150 (Bind Abbr) v) (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead d (Bind Abbr) v)
1151 i H (CHead x0 (Bind Abbr) x1) H5)) in (\lambda (H11: (eq C d x0)).(let H12
1152 \def (eq_ind_r T x1 (\lambda (t: T).(getl i c (CHead x0 (Bind Abbr) t))) H8 v
1153 H10) in (eq_ind T v (\lambda (t: T).(sn3 c (lift (S i) O t))) (let H13 \def
1154 (eq_ind_r C x0 (\lambda (c0: C).(getl i c (CHead c0 (Bind Abbr) v))) H12 d
1155 H11) in (sn3_lift d v H0 c (S i) O (getl_drop Abbr c d v i H13))) x1 H10))))
1156 H9))) t2 H6)))))) H4)) H3))))))))))).
1159 \forall (c: C).(\forall (d: C).(\forall (h: nat).(\forall (i: nat).((drop h
1160 i c d) \to (\forall (ts: TList).((sns3 d ts) \to (sns3 c (lifts h i ts))))))))
1162 \lambda (c: C).(\lambda (d: C).(\lambda (h: nat).(\lambda (i: nat).(\lambda
1163 (H: (drop h i c d)).(\lambda (ts: TList).(TList_ind (\lambda (t:
1164 TList).((sns3 d t) \to (sns3 c (lifts h i t)))) (\lambda (H0: True).H0)
1165 (\lambda (t: T).(\lambda (t0: TList).(\lambda (H0: (((sns3 d t0) \to (sns3 c
1166 (lifts h i t0))))).(\lambda (H1: (land (sn3 d t) (sns3 d t0))).(let H2 \def
1167 H1 in (and_ind (sn3 d t) (sns3 d t0) (land (sn3 c (lift h i t)) (sns3 c
1168 (lifts h i t0))) (\lambda (H3: (sn3 d t)).(\lambda (H4: (sns3 d t0)).(conj
1169 (sn3 c (lift h i t)) (sns3 c (lifts h i t0)) (sn3_lift d t H3 c h i H) (H0
1170 H4)))) H2)))))) ts)))))).
projects / helm.git / blob