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_head_12 c x x2 (pr3_pr2 c
430 x x2 H18) (Flat Appl) x0 x4 (pr3_pr2 (CHead c (Flat Appl) x2) x0 x4
431 (pr2_cflat c x0 x4 H24 Appl x2))) x2 x4 (refl_equal T (THead (Flat Appl) x2
432 x4)) x5 (H10 (THead (Flat Appl) x2 x5) H30 (pr3_head_12 c x x2 (pr3_pr2 c x
433 x2 H18) (Flat Appl) x1 x5 (pr3_pr2 (CHead c (Flat Appl) x2) x1 x5 (pr2_cflat
434 c x1 x5 H25 Appl x2)))))) H29)))) H27))) x3 H23))))))) H22)) (\lambda (H22:
435 (pr2 c x1 x3)).(let H_x \def (term_dec (THead (Flat Appl) x x1) (THead (Flat
436 Appl) x2 x3)) in (let H23 \def H_x in (or_ind (eq T (THead (Flat Appl) x x1)
437 (THead (Flat Appl) x2 x3)) ((eq T (THead (Flat Appl) x x1) (THead (Flat Appl)
438 x2 x3)) \to (\forall (P: Prop).P)) (sn3 c (THead (Flat Appl) x2 x3)) (\lambda
439 (H24: (eq T (THead (Flat Appl) x x1) (THead (Flat Appl) x2 x3))).(let H25
440 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
441 with [(TSort _) \Rightarrow x | (TLRef _) \Rightarrow x | (THead _ t3 _)
442 \Rightarrow t3])) (THead (Flat Appl) x x1) (THead (Flat Appl) x2 x3) H24) in
443 ((let H26 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_:
444 T).T) with [(TSort _) \Rightarrow x1 | (TLRef _) \Rightarrow x1 | (THead _ _
445 t3) \Rightarrow t3])) (THead (Flat Appl) x x1) (THead (Flat Appl) x2 x3) H24)
446 in (\lambda (H27: (eq T x x2)).(let H28 \def (eq_ind_r T x3 (\lambda (t3:
447 T).(pr2 c x1 t3)) H22 x1 H26) in (let H29 \def (eq_ind_r T x3 (\lambda (t3:
448 T).((eq T (THead (Flat Appl) x (THead (Flat Cast) x0 x1)) (THead (Flat Appl)
449 x2 t3)) \to (\forall (P: Prop).P))) H20 x1 H26) in (eq_ind T x1 (\lambda (t3:
450 T).(sn3 c (THead (Flat Appl) x2 t3))) (let H30 \def (eq_ind_r T x2 (\lambda
451 (t3: T).((eq T (THead (Flat Appl) x (THead (Flat Cast) x0 x1)) (THead (Flat
452 Appl) t3 x1)) \to (\forall (P: Prop).P))) H29 x H27) in (let H31 \def
453 (eq_ind_r T x2 (\lambda (t3: T).(pr2 c x t3)) H18 x H27) in (eq_ind T x
454 (\lambda (t3: T).(sn3 c (THead (Flat Appl) t3 x1))) (sn3_sing c (THead (Flat
455 Appl) x x1) H10) x2 H27))) x3 H26))))) H25))) (\lambda (H24: (((eq T (THead
456 (Flat Appl) x x1) (THead (Flat Appl) x2 x3)) \to (\forall (P:
457 Prop).P)))).(H10 (THead (Flat Appl) x2 x3) H24 (pr3_head_12 c x x2 (pr3_pr2 c
458 x x2 H18) (Flat Appl) x1 x3 (pr3_pr2 (CHead c (Flat Appl) x2) x1 x3
459 (pr2_cflat c x1 x3 H22 Appl x2))))) H23)))) H21)) t2 H17))))))) H16))
460 (\lambda (H16: (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
461 T).(\lambda (_: T).(eq T (THead (Flat Cast) x0 x1) (THead (Bind Abst) y1
462 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3:
463 T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
464 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda (_: T).(\lambda
465 (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u0:
466 T).(pr2 (CHead c (Bind b) u0) z1 t3))))))))).(ex4_4_ind T T T T (\lambda (y1:
467 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Cast)
468 x0 x1) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_:
469 T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3))))))
470 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x
471 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3:
472 T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b) u0) z1 t3)))))))
473 (sn3 c t2) (\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda (x5:
474 T).(\lambda (H17: (eq T (THead (Flat Cast) x0 x1) (THead (Bind Abst) x2
475 x3))).(\lambda (H18: (eq T t2 (THead (Bind Abbr) x4 x5))).(\lambda (_: (pr2 c
476 x x4)).(\lambda (_: ((\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b)
477 u0) x3 x5))))).(let H21 \def (eq_ind T t2 (\lambda (t3: T).((eq T (THead
478 (Flat Appl) x (THead (Flat Cast) x0 x1)) t3) \to (\forall (P: Prop).P))) H13
479 (THead (Bind Abbr) x4 x5) H18) in (eq_ind_r T (THead (Bind Abbr) x4 x5)
480 (\lambda (t3: T).(sn3 c t3)) (let H22 \def (eq_ind T (THead (Flat Cast) x0
481 x1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
482 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
483 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
484 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abst) x2
485 x3) H17) in (False_ind (sn3 c (THead (Bind Abbr) x4 x5)) H22)) t2
486 H18)))))))))) H16)) (\lambda (H16: (ex6_6 B T T T T T (\lambda (b:
487 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
488 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
489 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat
490 Cast) x0 x1) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
491 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
492 t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
493 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
494 T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1:
495 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
496 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
497 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1
498 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda
499 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b
500 Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
501 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Cast) x0 x1) (THead
502 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
503 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
504 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
505 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
506 (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
507 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
508 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
509 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))) (sn3 c t2)
510 (\lambda (x2: B).(\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda
511 (x6: T).(\lambda (x7: T).(\lambda (_: (not (eq B x2 Abst))).(\lambda (H18:
512 (eq T (THead (Flat Cast) x0 x1) (THead (Bind x2) x3 x4))).(\lambda (H19: (eq
513 T t2 (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) O x6) x5)))).(\lambda
514 (_: (pr2 c x x6)).(\lambda (_: (pr2 c x3 x7)).(\lambda (_: (pr2 (CHead c
515 (Bind x2) x7) x4 x5)).(let H23 \def (eq_ind T t2 (\lambda (t3: T).((eq T
516 (THead (Flat Appl) x (THead (Flat Cast) x0 x1)) t3) \to (\forall (P:
517 Prop).P))) H13 (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) O x6) x5))
518 H19) in (eq_ind_r T (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) O x6)
519 x5)) (\lambda (t3: T).(sn3 c t3)) (let H24 \def (eq_ind T (THead (Flat Cast)
520 x0 x1) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with
521 [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
522 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
523 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind x2) x3 x4)
524 H18) in (False_ind (sn3 c (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O)
525 O x6) x5))) H24)) t2 H19)))))))))))))) H16)) H15))))))))))))))) y0 H5))))
526 H4))))))))) y H0))))) H)))).
528 theorem sn3_appl_appl:
529 \forall (v1: T).(\forall (t1: T).(let u1 \def (THead (Flat Appl) v1 t1) in
530 (\forall (c: C).((sn3 c u1) \to (\forall (v2: T).((sn3 c v2) \to (((\forall
531 (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to (\forall (P: Prop).P))) \to
532 (sn3 c (THead (Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2
535 \lambda (v1: T).(\lambda (t1: T).(let u1 \def (THead (Flat Appl) v1 t1) in
536 (\lambda (c: C).(\lambda (H: (sn3 c (THead (Flat Appl) v1 t1))).(insert_eq T
537 (THead (Flat Appl) v1 t1) (\lambda (t: T).(sn3 c t)) (\forall (v2: T).((sn3 c
538 v2) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) v1 t1) u2) \to ((((iso
539 (THead (Flat Appl) v1 t1) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead
540 (Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2 (THead (Flat Appl)
541 v1 t1)))))) (\lambda (y: T).(\lambda (H0: (sn3 c y)).(unintro T t1 (\lambda
542 (t: T).((eq T y (THead (Flat Appl) v1 t)) \to (\forall (v2: T).((sn3 c v2)
543 \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) v1 t) u2) \to ((((iso
544 (THead (Flat Appl) v1 t) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead
545 (Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2 (THead (Flat Appl)
546 v1 t)))))))) (unintro T v1 (\lambda (t: T).(\forall (x: T).((eq T y (THead
547 (Flat Appl) t x)) \to (\forall (v2: T).((sn3 c v2) \to (((\forall (u2:
548 T).((pr3 c (THead (Flat Appl) t x) u2) \to ((((iso (THead (Flat Appl) t x)
549 u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to
550 (sn3 c (THead (Flat Appl) v2 (THead (Flat Appl) t x))))))))) (sn3_ind c
551 (\lambda (t: T).(\forall (x: T).(\forall (x0: T).((eq T t (THead (Flat Appl)
552 x x0)) \to (\forall (v2: T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c (THead
553 (Flat Appl) x x0) u2) \to ((((iso (THead (Flat Appl) x x0) u2) \to (\forall
554 (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to (sn3 c (THead
555 (Flat Appl) v2 (THead (Flat Appl) x x0)))))))))) (\lambda (t2: T).(\lambda
556 (H1: ((\forall (t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P))) \to ((pr3
557 c t2 t3) \to (sn3 c t3)))))).(\lambda (H2: ((\forall (t3: T).((((eq T t2 t3)
558 \to (\forall (P: Prop).P))) \to ((pr3 c t2 t3) \to (\forall (x: T).(\forall
559 (x0: T).((eq T t3 (THead (Flat Appl) x x0)) \to (\forall (v2: T).((sn3 c v2)
560 \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x x0) u2) \to ((((iso
561 (THead (Flat Appl) x x0) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead
562 (Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2 (THead (Flat Appl) x
563 x0)))))))))))))).(\lambda (x: T).(\lambda (x0: T).(\lambda (H3: (eq T t2
564 (THead (Flat Appl) x x0))).(\lambda (v2: T).(\lambda (H4: (sn3 c
565 v2)).(sn3_ind c (\lambda (t: T).(((\forall (u2: T).((pr3 c (THead (Flat Appl)
566 x x0) u2) \to ((((iso (THead (Flat Appl) x x0) u2) \to (\forall (P:
567 Prop).P))) \to (sn3 c (THead (Flat Appl) t u2)))))) \to (sn3 c (THead (Flat
568 Appl) t (THead (Flat Appl) x x0))))) (\lambda (t0: T).(\lambda (H5: ((\forall
569 (t3: T).((((eq T t0 t3) \to (\forall (P: Prop).P))) \to ((pr3 c t0 t3) \to
570 (sn3 c t3)))))).(\lambda (H6: ((\forall (t3: T).((((eq T t0 t3) \to (\forall
571 (P: Prop).P))) \to ((pr3 c t0 t3) \to (((\forall (u2: T).((pr3 c (THead (Flat
572 Appl) x x0) u2) \to ((((iso (THead (Flat Appl) x x0) u2) \to (\forall (P:
573 Prop).P))) \to (sn3 c (THead (Flat Appl) t3 u2)))))) \to (sn3 c (THead (Flat
574 Appl) t3 (THead (Flat Appl) x x0))))))))).(\lambda (H7: ((\forall (u2:
575 T).((pr3 c (THead (Flat Appl) x x0) u2) \to ((((iso (THead (Flat Appl) x x0)
576 u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) t0
577 u2))))))).(let H8 \def (eq_ind T t2 (\lambda (t: T).(\forall (t3: T).((((eq T
578 t t3) \to (\forall (P: Prop).P))) \to ((pr3 c t t3) \to (\forall (x1:
579 T).(\forall (x2: T).((eq T t3 (THead (Flat Appl) x1 x2)) \to (\forall (v3:
580 T).((sn3 c v3) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x1 x2) u2)
581 \to ((((iso (THead (Flat Appl) x1 x2) u2) \to (\forall (P: Prop).P))) \to
582 (sn3 c (THead (Flat Appl) v3 u2)))))) \to (sn3 c (THead (Flat Appl) v3 (THead
583 (Flat Appl) x1 x2))))))))))))) H2 (THead (Flat Appl) x x0) H3) in (let H9
584 \def (eq_ind T t2 (\lambda (t: T).(\forall (t3: T).((((eq T t t3) \to
585 (\forall (P: Prop).P))) \to ((pr3 c t t3) \to (sn3 c t3))))) H1 (THead (Flat
586 Appl) x x0) H3) in (sn3_pr2_intro c (THead (Flat Appl) t0 (THead (Flat Appl)
587 x x0)) (\lambda (t3: T).(\lambda (H10: (((eq T (THead (Flat Appl) t0 (THead
588 (Flat Appl) x x0)) t3) \to (\forall (P: Prop).P)))).(\lambda (H11: (pr2 c
589 (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t3)).(let H12 \def
590 (pr2_gen_appl c t0 (THead (Flat Appl) x x0) t3 H11) in (or3_ind (ex3_2 T T
591 (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 t4))))
592 (\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2))) (\lambda (_: T).(\lambda
593 (t4: T).(pr2 c (THead (Flat Appl) x x0) t4)))) (ex4_4 T T T T (\lambda (y1:
594 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Appl)
595 x x0) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda
596 (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
597 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2)))))
598 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall
599 (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4)))))))) (ex6_6 B T T T
600 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
601 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
602 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq
603 T (THead (Flat Appl) x x0) (THead (Bind b) y1 z1)))))))) (\lambda (b:
604 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
605 (y2: T).(eq T t3 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2)
606 z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
607 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2))))))) (\lambda (_:
608 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
609 (y2: T).(pr2 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
610 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b)
611 y2) z1 z2)))))))) (sn3 c t3) (\lambda (H13: (ex3_2 T T (\lambda (u2:
612 T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2:
613 T).(\lambda (_: T).(pr2 c t0 u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c
614 (THead (Flat Appl) x x0) t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda
615 (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_:
616 T).(pr2 c t0 u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c (THead (Flat Appl)
617 x x0) t4))) (sn3 c t3) (\lambda (x1: T).(\lambda (x2: T).(\lambda (H14: (eq T
618 t3 (THead (Flat Appl) x1 x2))).(\lambda (H15: (pr2 c t0 x1)).(\lambda (H16:
619 (pr2 c (THead (Flat Appl) x x0) x2)).(let H17 \def (eq_ind T t3 (\lambda (t:
620 T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t) \to (\forall (P:
621 Prop).P))) H10 (THead (Flat Appl) x1 x2) H14) in (eq_ind_r T (THead (Flat
622 Appl) x1 x2) (\lambda (t: T).(sn3 c t)) (let H18 \def (pr2_gen_appl c x x0 x2
623 H16) in (or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T x2 (THead
624 (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
625 (\lambda (_: T).(\lambda (t4: T).(pr2 c x0 t4)))) (ex4_4 T T T T (\lambda
626 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T x0 (THead
627 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
628 T).(\lambda (t4: T).(eq T x2 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
629 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
630 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b:
631 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4)))))))) (ex6_6 B T T T T T
632 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
633 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
634 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T x0
635 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
636 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T x2 (THead (Bind
637 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
638 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
639 (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
640 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
641 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
642 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))) (sn3 c
643 (THead (Flat Appl) x1 x2)) (\lambda (H19: (ex3_2 T T (\lambda (u2:
644 T).(\lambda (t4: T).(eq T x2 (THead (Flat Appl) u2 t4)))) (\lambda (u2:
645 T).(\lambda (_: T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c x0
646 t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t4: T).(eq T x2 (THead
647 (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
648 (\lambda (_: T).(\lambda (t4: T).(pr2 c x0 t4))) (sn3 c (THead (Flat Appl) x1
649 x2)) (\lambda (x3: T).(\lambda (x4: T).(\lambda (H20: (eq T x2 (THead (Flat
650 Appl) x3 x4))).(\lambda (H21: (pr2 c x x3)).(\lambda (H22: (pr2 c x0
651 x4)).(let H23 \def (eq_ind T x2 (\lambda (t: T).((eq T (THead (Flat Appl) t0
652 (THead (Flat Appl) x x0)) (THead (Flat Appl) x1 t)) \to (\forall (P:
653 Prop).P))) H17 (THead (Flat Appl) x3 x4) H20) in (eq_ind_r T (THead (Flat
654 Appl) x3 x4) (\lambda (t: T).(sn3 c (THead (Flat Appl) x1 t))) (let H_x \def
655 (term_dec (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4)) in (let H24
656 \def H_x in (or_ind (eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4))
657 ((eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4)) \to (\forall (P:
658 Prop).P)) (sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))) (\lambda
659 (H25: (eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4))).(let H26
660 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
661 with [(TSort _) \Rightarrow x | (TLRef _) \Rightarrow x | (THead _ t _)
662 \Rightarrow t])) (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4) H25) in
663 ((let H27 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_:
664 T).T) with [(TSort _) \Rightarrow x0 | (TLRef _) \Rightarrow x0 | (THead _ _
665 t) \Rightarrow t])) (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4) H25)
666 in (\lambda (H28: (eq T x x3)).(let H29 \def (eq_ind_r T x4 (\lambda (t:
667 T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) (THead (Flat Appl)
668 x1 (THead (Flat Appl) x3 t))) \to (\forall (P: Prop).P))) H23 x0 H27) in (let
669 H30 \def (eq_ind_r T x4 (\lambda (t: T).(pr2 c x0 t)) H22 x0 H27) in (eq_ind
670 T x0 (\lambda (t: T).(sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 t))))
671 (let H31 \def (eq_ind_r T x3 (\lambda (t: T).((eq T (THead (Flat Appl) t0
672 (THead (Flat Appl) x x0)) (THead (Flat Appl) x1 (THead (Flat Appl) t x0)))
673 \to (\forall (P: Prop).P))) H29 x H28) in (let H32 \def (eq_ind_r T x3
674 (\lambda (t: T).(pr2 c x t)) H21 x H28) in (eq_ind T x (\lambda (t: T).(sn3 c
675 (THead (Flat Appl) x1 (THead (Flat Appl) t x0)))) (let H_x0 \def (term_dec t0
676 x1) in (let H33 \def H_x0 in (or_ind (eq T t0 x1) ((eq T t0 x1) \to (\forall
677 (P: Prop).P)) (sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x x0)))
678 (\lambda (H34: (eq T t0 x1)).(let H35 \def (eq_ind_r T x1 (\lambda (t:
679 T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) (THead (Flat Appl)
680 t (THead (Flat Appl) x x0))) \to (\forall (P: Prop).P))) H31 t0 H34) in (let
681 H36 \def (eq_ind_r T x1 (\lambda (t: T).(pr2 c t0 t)) H15 t0 H34) in (eq_ind
682 T t0 (\lambda (t: T).(sn3 c (THead (Flat Appl) t (THead (Flat Appl) x x0))))
683 (H35 (refl_equal T (THead (Flat Appl) t0 (THead (Flat Appl) x x0))) (sn3 c
684 (THead (Flat Appl) t0 (THead (Flat Appl) x x0)))) x1 H34)))) (\lambda (H34:
685 (((eq T t0 x1) \to (\forall (P: Prop).P)))).(H6 x1 H34 (pr3_pr2 c t0 x1 H15)
686 (\lambda (u2: T).(\lambda (H35: (pr3 c (THead (Flat Appl) x x0) u2)).(\lambda
687 (H36: (((iso (THead (Flat Appl) x x0) u2) \to (\forall (P:
688 Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t0 u2) (H7 u2 H35 H36) (THead
689 (Flat Appl) x1 u2) (pr3_pr2 c (THead (Flat Appl) t0 u2) (THead (Flat Appl) x1
690 u2) (pr2_head_1 c t0 x1 H15 (Flat Appl) u2)))))))) H33))) x3 H28))) x4
691 H27))))) H26))) (\lambda (H25: (((eq T (THead (Flat Appl) x x0) (THead (Flat
692 Appl) x3 x4)) \to (\forall (P: Prop).P)))).(H8 (THead (Flat Appl) x3 x4) H25
693 (pr3_head_12 c x x3 (pr3_pr2 c x x3 H21) (Flat Appl) x0 x4 (pr3_pr2 (CHead c
694 (Flat Appl) x3) x0 x4 (pr2_cflat c x0 x4 H22 Appl x3))) x3 x4 (refl_equal T
695 (THead (Flat Appl) x3 x4)) x1 (sn3_pr3_trans c t0 (sn3_sing c t0 H5) x1
696 (pr3_pr2 c t0 x1 H15)) (\lambda (u2: T).(\lambda (H26: (pr3 c (THead (Flat
697 Appl) x3 x4) u2)).(\lambda (H27: (((iso (THead (Flat Appl) x3 x4) u2) \to
698 (\forall (P: Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t0 u2) (H7 u2
699 (pr3_sing c (THead (Flat Appl) x x4) (THead (Flat Appl) x x0) (pr2_thin_dx c
700 x0 x4 H22 x Appl) u2 (pr3_sing c (THead (Flat Appl) x3 x4) (THead (Flat Appl)
701 x x4) (pr2_head_1 c x x3 H21 (Flat Appl) x4) u2 H26)) (\lambda (H28: (iso
702 (THead (Flat Appl) x x0) u2)).(\lambda (P: Prop).(H27 (iso_trans (THead (Flat
703 Appl) x3 x4) (THead (Flat Appl) x x0) (iso_head (Flat Appl) x3 x x4 x0) u2
704 H28) P)))) (THead (Flat Appl) x1 u2) (pr3_pr2 c (THead (Flat Appl) t0 u2)
705 (THead (Flat Appl) x1 u2) (pr2_head_1 c t0 x1 H15 (Flat Appl) u2))))))))
706 H24))) x2 H20))))))) H19)) (\lambda (H19: (ex4_4 T T T T (\lambda (y1:
707 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T x0 (THead (Bind
708 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
709 (t4: T).(eq T x2 (THead (Bind Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_:
710 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda (_: T).(\lambda
711 (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b: B).(\forall (u: T).(pr2
712 (CHead c (Bind b) u) z1 t4))))))))).(ex4_4_ind T T T T (\lambda (y1:
713 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T x0 (THead (Bind
714 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
715 (t4: T).(eq T x2 (THead (Bind Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_:
716 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda (_: T).(\lambda
717 (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b: B).(\forall (u: T).(pr2
718 (CHead c (Bind b) u) z1 t4))))))) (sn3 c (THead (Flat Appl) x1 x2)) (\lambda
719 (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda (x6: T).(\lambda (H20: (eq
720 T x0 (THead (Bind Abst) x3 x4))).(\lambda (H21: (eq T x2 (THead (Bind Abbr)
721 x5 x6))).(\lambda (H22: (pr2 c x x5)).(\lambda (H23: ((\forall (b:
722 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x4 x6))))).(let H24 \def (eq_ind
723 T x2 (\lambda (t: T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0))
724 (THead (Flat Appl) x1 t)) \to (\forall (P: Prop).P))) H17 (THead (Bind Abbr)
725 x5 x6) H21) in (eq_ind_r T (THead (Bind Abbr) x5 x6) (\lambda (t: T).(sn3 c
726 (THead (Flat Appl) x1 t))) (let H25 \def (eq_ind T x0 (\lambda (t: T).((eq T
727 (THead (Flat Appl) t0 (THead (Flat Appl) x t)) (THead (Flat Appl) x1 (THead
728 (Bind Abbr) x5 x6))) \to (\forall (P: Prop).P))) H24 (THead (Bind Abst) x3
729 x4) H20) in (let H26 \def (eq_ind T x0 (\lambda (t: T).(\forall (t4:
730 T).((((eq T (THead (Flat Appl) x t) t4) \to (\forall (P: Prop).P))) \to ((pr3
731 c (THead (Flat Appl) x t) t4) \to (sn3 c t4))))) H9 (THead (Bind Abst) x3 x4)
732 H20) in (let H27 \def (eq_ind T x0 (\lambda (t: T).(\forall (t4: T).((((eq T
733 (THead (Flat Appl) x t) t4) \to (\forall (P: Prop).P))) \to ((pr3 c (THead
734 (Flat Appl) x t) t4) \to (\forall (x7: T).(\forall (x8: T).((eq T t4 (THead
735 (Flat Appl) x7 x8)) \to (\forall (v3: T).((sn3 c v3) \to (((\forall (u2:
736 T).((pr3 c (THead (Flat Appl) x7 x8) u2) \to ((((iso (THead (Flat Appl) x7
737 x8) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v3 u2))))))
738 \to (sn3 c (THead (Flat Appl) v3 (THead (Flat Appl) x7 x8))))))))))))) H8
739 (THead (Bind Abst) x3 x4) H20) in (let H28 \def (eq_ind T x0 (\lambda (t:
740 T).(\forall (u2: T).((pr3 c (THead (Flat Appl) x t) u2) \to ((((iso (THead
741 (Flat Appl) x t) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat
742 Appl) t0 u2)))))) H7 (THead (Bind Abst) x3 x4) H20) in (let H29 \def (eq_ind
743 T x0 (\lambda (t: T).(\forall (t4: T).((((eq T t0 t4) \to (\forall (P:
744 Prop).P))) \to ((pr3 c t0 t4) \to (((\forall (u2: T).((pr3 c (THead (Flat
745 Appl) x t) u2) \to ((((iso (THead (Flat Appl) x t) u2) \to (\forall (P:
746 Prop).P))) \to (sn3 c (THead (Flat Appl) t4 u2)))))) \to (sn3 c (THead (Flat
747 Appl) t4 (THead (Flat Appl) x t)))))))) H6 (THead (Bind Abst) x3 x4) H20) in
748 (sn3_pr3_trans c (THead (Flat Appl) t0 (THead (Bind Abbr) x5 x6)) (H28 (THead
749 (Bind Abbr) x5 x6) (pr3_sing c (THead (Bind Abbr) x x4) (THead (Flat Appl) x
750 (THead (Bind Abst) x3 x4)) (pr2_free c (THead (Flat Appl) x (THead (Bind
751 Abst) x3 x4)) (THead (Bind Abbr) x x4) (pr0_beta x3 x x (pr0_refl x) x4 x4
752 (pr0_refl x4))) (THead (Bind Abbr) x5 x6) (pr3_head_12 c x x5 (pr3_pr2 c x x5
753 H22) (Bind Abbr) x4 x6 (pr3_pr2 (CHead c (Bind Abbr) x5) x4 x6 (H23 Abbr
754 x5)))) (\lambda (H30: (iso (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
755 (THead (Bind Abbr) x5 x6))).(\lambda (P: Prop).(let H31 \def (match H30 in
756 iso return (\lambda (t: T).(\lambda (t4: T).(\lambda (_: (iso t t4)).((eq T t
757 (THead (Flat Appl) x (THead (Bind Abst) x3 x4))) \to ((eq T t4 (THead (Bind
758 Abbr) x5 x6)) \to P))))) with [(iso_sort n1 n2) \Rightarrow (\lambda (H31:
759 (eq T (TSort n1) (THead (Flat Appl) x (THead (Bind Abst) x3 x4)))).(\lambda
760 (H32: (eq T (TSort n2) (THead (Bind Abbr) x5 x6))).((let H33 \def (eq_ind T
761 (TSort n1) (\lambda (e: T).(match e in T return (\lambda (_: T).Prop) with
762 [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _)
763 \Rightarrow False])) I (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) H31)
764 in (False_ind ((eq T (TSort n2) (THead (Bind Abbr) x5 x6)) \to P) H33))
765 H32))) | (iso_lref i1 i2) \Rightarrow (\lambda (H31: (eq T (TLRef i1) (THead
766 (Flat Appl) x (THead (Bind Abst) x3 x4)))).(\lambda (H32: (eq T (TLRef i2)
767 (THead (Bind Abbr) x5 x6))).((let H33 \def (eq_ind T (TLRef i1) (\lambda (e:
768 T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
769 False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
770 (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) H31) in (False_ind ((eq T
771 (TLRef i2) (THead (Bind Abbr) x5 x6)) \to P) H33)) H32))) | (iso_head k v4 v5
772 t4 t5) \Rightarrow (\lambda (H31: (eq T (THead k v4 t4) (THead (Flat Appl) x
773 (THead (Bind Abst) x3 x4)))).(\lambda (H32: (eq T (THead k v5 t5) (THead
774 (Bind Abbr) x5 x6))).((let H33 \def (f_equal T T (\lambda (e: T).(match e in
775 T return (\lambda (_: T).T) with [(TSort _) \Rightarrow t4 | (TLRef _)
776 \Rightarrow t4 | (THead _ _ t) \Rightarrow t])) (THead k v4 t4) (THead (Flat
777 Appl) x (THead (Bind Abst) x3 x4)) H31) in ((let H34 \def (f_equal T T
778 (\lambda (e: T).(match e in T return (\lambda (_: T).T) with [(TSort _)
779 \Rightarrow v4 | (TLRef _) \Rightarrow v4 | (THead _ t _) \Rightarrow t]))
780 (THead k v4 t4) (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) H31) in ((let
781 H35 \def (f_equal T K (\lambda (e: T).(match e in T return (\lambda (_: T).K)
782 with [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _)
783 \Rightarrow k0])) (THead k v4 t4) (THead (Flat Appl) x (THead (Bind Abst) x3
784 x4)) H31) in (eq_ind K (Flat Appl) (\lambda (k0: K).((eq T v4 x) \to ((eq T
785 t4 (THead (Bind Abst) x3 x4)) \to ((eq T (THead k0 v5 t5) (THead (Bind Abbr)
786 x5 x6)) \to P)))) (\lambda (H36: (eq T v4 x)).(eq_ind T x (\lambda (_:
787 T).((eq T t4 (THead (Bind Abst) x3 x4)) \to ((eq T (THead (Flat Appl) v5 t5)
788 (THead (Bind Abbr) x5 x6)) \to P))) (\lambda (H37: (eq T t4 (THead (Bind
789 Abst) x3 x4))).(eq_ind T (THead (Bind Abst) x3 x4) (\lambda (_: T).((eq T
790 (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6)) \to P)) (\lambda (H38:
791 (eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6))).(let H39 \def
792 (eq_ind T (THead (Flat Appl) v5 t5) (\lambda (e: T).(match e in T return
793 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
794 \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in K return (\lambda
795 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
796 True])])) I (THead (Bind Abbr) x5 x6) H38) in (False_ind P H39))) t4 (sym_eq
797 T t4 (THead (Bind Abst) x3 x4) H37))) v4 (sym_eq T v4 x H36))) k (sym_eq K k
798 (Flat Appl) H35))) H34)) H33)) H32)))]) in (H31 (refl_equal T (THead (Flat
799 Appl) x (THead (Bind Abst) x3 x4))) (refl_equal T (THead (Bind Abbr) x5
800 x6))))))) (THead (Flat Appl) x1 (THead (Bind Abbr) x5 x6)) (pr3_pr2 c (THead
801 (Flat Appl) t0 (THead (Bind Abbr) x5 x6)) (THead (Flat Appl) x1 (THead (Bind
802 Abbr) x5 x6)) (pr2_head_1 c t0 x1 H15 (Flat Appl) (THead (Bind Abbr) x5
803 x6))))))))) x2 H21)))))))))) H19)) (\lambda (H19: (ex6_6 B T T T T T (\lambda
804 (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
805 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
806 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T x0
807 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
808 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T x2 (THead (Bind
809 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
810 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
811 (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
812 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
813 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
814 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))))).(ex6_6_ind
815 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
816 T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
817 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
818 (_: T).(eq T x0 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
819 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
820 x2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
821 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
822 T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1:
823 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
824 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
825 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))
826 (sn3 c (THead (Flat Appl) x1 x2)) (\lambda (x3: B).(\lambda (x4: T).(\lambda
827 (x5: T).(\lambda (x6: T).(\lambda (x7: T).(\lambda (x8: T).(\lambda (H20:
828 (not (eq B x3 Abst))).(\lambda (H21: (eq T x0 (THead (Bind x3) x4
829 x5))).(\lambda (H22: (eq T x2 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S
830 O) O x7) x6)))).(\lambda (H23: (pr2 c x x7)).(\lambda (H24: (pr2 c x4
831 x8)).(\lambda (H25: (pr2 (CHead c (Bind x3) x8) x5 x6)).(let H26 \def (eq_ind
832 T x2 (\lambda (t: T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0))
833 (THead (Flat Appl) x1 t)) \to (\forall (P: Prop).P))) H17 (THead (Bind x3) x8
834 (THead (Flat Appl) (lift (S O) O x7) x6)) H22) in (eq_ind_r T (THead (Bind
835 x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)) (\lambda (t: T).(sn3 c
836 (THead (Flat Appl) x1 t))) (let H27 \def (eq_ind T x0 (\lambda (t: T).((eq T
837 (THead (Flat Appl) t0 (THead (Flat Appl) x t)) (THead (Flat Appl) x1 (THead
838 (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)))) \to (\forall (P:
839 Prop).P))) H26 (THead (Bind x3) x4 x5) H21) in (let H28 \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 (sn3 c
842 t4))))) H9 (THead (Bind x3) x4 x5) H21) in (let H29 \def (eq_ind T x0
843 (\lambda (t: T).(\forall (t4: T).((((eq T (THead (Flat Appl) x t) t4) \to
844 (\forall (P: Prop).P))) \to ((pr3 c (THead (Flat Appl) x t) t4) \to (\forall
845 (x9: T).(\forall (x10: T).((eq T t4 (THead (Flat Appl) x9 x10)) \to (\forall
846 (v3: T).((sn3 c v3) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x9 x10)
847 u2) \to ((((iso (THead (Flat Appl) x9 x10) u2) \to (\forall (P: Prop).P)))
848 \to (sn3 c (THead (Flat Appl) v3 u2)))))) \to (sn3 c (THead (Flat Appl) v3
849 (THead (Flat Appl) x9 x10))))))))))))) H8 (THead (Bind x3) x4 x5) H21) in
850 (let H30 \def (eq_ind T x0 (\lambda (t: T).(\forall (u2: T).((pr3 c (THead
851 (Flat Appl) x t) u2) \to ((((iso (THead (Flat Appl) x t) u2) \to (\forall (P:
852 Prop).P))) \to (sn3 c (THead (Flat Appl) t0 u2)))))) H7 (THead (Bind x3) x4
853 x5) H21) in (let H31 \def (eq_ind T x0 (\lambda (t: T).(\forall (t4:
854 T).((((eq T t0 t4) \to (\forall (P: Prop).P))) \to ((pr3 c t0 t4) \to
855 (((\forall (u2: T).((pr3 c (THead (Flat Appl) x t) u2) \to ((((iso (THead
856 (Flat Appl) x t) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat
857 Appl) t4 u2)))))) \to (sn3 c (THead (Flat Appl) t4 (THead (Flat Appl) x
858 t)))))))) H6 (THead (Bind x3) x4 x5) H21) in (sn3_pr3_trans c (THead (Flat
859 Appl) t0 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) (H30
860 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)) (pr3_sing c
861 (THead (Bind x3) x4 (THead (Flat Appl) (lift (S O) O x) x5)) (THead (Flat
862 Appl) x (THead (Bind x3) x4 x5)) (pr2_free c (THead (Flat Appl) x (THead
863 (Bind x3) x4 x5)) (THead (Bind x3) x4 (THead (Flat Appl) (lift (S O) O x)
864 x5)) (pr0_upsilon x3 H20 x x (pr0_refl x) x4 x4 (pr0_refl x4) x5 x5 (pr0_refl
865 x5))) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
866 (pr3_head_12 c x4 x8 (pr3_pr2 c x4 x8 H24) (Bind x3) (THead (Flat Appl) (lift
867 (S O) O x) x5) (THead (Flat Appl) (lift (S O) O x7) x6) (pr3_head_12 (CHead c
868 (Bind x3) x8) (lift (S O) O x) (lift (S O) O x7) (pr3_lift (CHead c (Bind x3)
869 x8) c (S O) O (drop_drop (Bind x3) O c c (drop_refl c) x8) x x7 (pr3_pr2 c x
870 x7 H23)) (Flat Appl) x5 x6 (pr3_pr2 (CHead (CHead c (Bind x3) x8) (Flat Appl)
871 (lift (S O) O x7)) x5 x6 (pr2_cflat (CHead c (Bind x3) x8) x5 x6 H25 Appl
872 (lift (S O) O x7)))))) (\lambda (H32: (iso (THead (Flat Appl) x (THead (Bind
873 x3) x4 x5)) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7)
874 x6)))).(\lambda (P: Prop).(let H33 \def (match H32 in iso return (\lambda (t:
875 T).(\lambda (t4: T).(\lambda (_: (iso t t4)).((eq T t (THead (Flat Appl) x
876 (THead (Bind x3) x4 x5))) \to ((eq T t4 (THead (Bind x3) x8 (THead (Flat
877 Appl) (lift (S O) O x7) x6))) \to P))))) with [(iso_sort n1 n2) \Rightarrow
878 (\lambda (H33: (eq T (TSort n1) (THead (Flat Appl) x (THead (Bind x3) x4
879 x5)))).(\lambda (H34: (eq T (TSort n2) (THead (Bind x3) x8 (THead (Flat Appl)
880 (lift (S O) O x7) x6)))).((let H35 \def (eq_ind T (TSort n1) (\lambda (e:
881 T).(match e in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow
882 True | (TLRef _) \Rightarrow False | (THead _ _ _) \Rightarrow False])) I
883 (THead (Flat Appl) x (THead (Bind x3) x4 x5)) H33) in (False_ind ((eq T
884 (TSort n2) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to
885 P) H35)) H34))) | (iso_lref i1 i2) \Rightarrow (\lambda (H33: (eq T (TLRef
886 i1) (THead (Flat Appl) x (THead (Bind x3) x4 x5)))).(\lambda (H34: (eq T
887 (TLRef i2) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7)
888 x6)))).((let H35 \def (eq_ind T (TLRef i1) (\lambda (e: T).(match e in T
889 return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
890 \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) x
891 (THead (Bind x3) x4 x5)) H33) in (False_ind ((eq T (TLRef i2) (THead (Bind
892 x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to P) H35)) H34))) |
893 (iso_head k v4 v5 t4 t5) \Rightarrow (\lambda (H33: (eq T (THead k v4 t4)
894 (THead (Flat Appl) x (THead (Bind x3) x4 x5)))).(\lambda (H34: (eq T (THead k
895 v5 t5) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)))).((let
896 H35 \def (f_equal T T (\lambda (e: T).(match e in T return (\lambda (_: T).T)
897 with [(TSort _) \Rightarrow t4 | (TLRef _) \Rightarrow t4 | (THead _ _ t)
898 \Rightarrow t])) (THead k v4 t4) (THead (Flat Appl) x (THead (Bind x3) x4
899 x5)) H33) in ((let H36 \def (f_equal T T (\lambda (e: T).(match e in T return
900 (\lambda (_: T).T) with [(TSort _) \Rightarrow v4 | (TLRef _) \Rightarrow v4
901 | (THead _ t _) \Rightarrow t])) (THead k v4 t4) (THead (Flat Appl) x (THead
902 (Bind x3) x4 x5)) H33) in ((let H37 \def (f_equal T K (\lambda (e: T).(match
903 e in T return (\lambda (_: T).K) with [(TSort _) \Rightarrow k | (TLRef _)
904 \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k v4 t4) (THead (Flat
905 Appl) x (THead (Bind x3) x4 x5)) H33) in (eq_ind K (Flat Appl) (\lambda (k0:
906 K).((eq T v4 x) \to ((eq T t4 (THead (Bind x3) x4 x5)) \to ((eq T (THead k0
907 v5 t5) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to
908 P)))) (\lambda (H38: (eq T v4 x)).(eq_ind T x (\lambda (_: T).((eq T t4
909 (THead (Bind x3) x4 x5)) \to ((eq T (THead (Flat Appl) v5 t5) (THead (Bind
910 x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to P))) (\lambda (H39: (eq
911 T t4 (THead (Bind x3) x4 x5))).(eq_ind T (THead (Bind x3) x4 x5) (\lambda (_:
912 T).((eq T (THead (Flat Appl) v5 t5) (THead (Bind x3) x8 (THead (Flat Appl)
913 (lift (S O) O x7) x6))) \to P)) (\lambda (H40: (eq T (THead (Flat Appl) v5
914 t5) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)))).(let H41
915 \def (eq_ind T (THead (Flat Appl) v5 t5) (\lambda (e: T).(match e in T return
916 (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef _)
917 \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 in K return (\lambda
918 (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
919 True])])) I (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
920 H40) in (False_ind P H41))) t4 (sym_eq T t4 (THead (Bind x3) x4 x5) H39))) v4
921 (sym_eq T v4 x H38))) k (sym_eq K k (Flat Appl) H37))) H36)) H35)) H34)))])
922 in (H33 (refl_equal T (THead (Flat Appl) x (THead (Bind x3) x4 x5)))
923 (refl_equal T (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7)
924 x6)))))))) (THead (Flat Appl) x1 (THead (Bind x3) x8 (THead (Flat Appl) (lift
925 (S O) O x7) x6))) (pr3_pr2 c (THead (Flat Appl) t0 (THead (Bind x3) x8 (THead
926 (Flat Appl) (lift (S O) O x7) x6))) (THead (Flat Appl) x1 (THead (Bind x3) x8
927 (THead (Flat Appl) (lift (S O) O x7) x6))) (pr2_head_1 c t0 x1 H15 (Flat
928 Appl) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))))))))))
929 x2 H22)))))))))))))) H19)) H18)) t3 H14))))))) H13)) (\lambda (H13: (ex4_4 T
930 T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
931 (THead (Flat Appl) x x0) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
932 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind
933 Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
934 (_: T).(pr2 c t0 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
935 T).(\lambda (t4: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
936 z1 t4))))))))).(ex4_4_ind T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
937 (_: T).(\lambda (_: T).(eq T (THead (Flat Appl) x x0) (THead (Bind Abst) y1
938 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t4:
939 T).(eq T t3 (THead (Bind Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_:
940 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2))))) (\lambda (_:
941 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b: B).(\forall
942 (u: T).(pr2 (CHead c (Bind b) u) z1 t4))))))) (sn3 c t3) (\lambda (x1:
943 T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda (H14: (eq T
944 (THead (Flat Appl) x x0) (THead (Bind Abst) x1 x2))).(\lambda (H15: (eq T t3
945 (THead (Bind Abbr) x3 x4))).(\lambda (_: (pr2 c t0 x3)).(\lambda (_:
946 ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x2 x4))))).(let
947 H18 \def (eq_ind T t3 (\lambda (t: T).((eq T (THead (Flat Appl) t0 (THead
948 (Flat Appl) x x0)) t) \to (\forall (P: Prop).P))) H10 (THead (Bind Abbr) x3
949 x4) H15) in (eq_ind_r T (THead (Bind Abbr) x3 x4) (\lambda (t: T).(sn3 c t))
950 (let H19 \def (eq_ind T (THead (Flat Appl) x x0) (\lambda (ee: T).(match ee
951 in T return (\lambda (_: T).Prop) with [(TSort _) \Rightarrow False | (TLRef
952 _) \Rightarrow False | (THead k _ _) \Rightarrow (match k in K return
953 (\lambda (_: K).Prop) with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow
954 True])])) I (THead (Bind Abst) x1 x2) H14) in (False_ind (sn3 c (THead (Bind
955 Abbr) x3 x4)) H19)) t3 H15)))))))))) H13)) (\lambda (H13: (ex6_6 B T T T T T
956 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
957 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
958 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T
959 (THead (Flat Appl) x x0) (THead (Bind b) y1 z1)))))))) (\lambda (b:
960 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
961 (y2: T).(eq T t3 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2)
962 z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
963 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2))))))) (\lambda (_:
964 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
965 (y2: T).(pr2 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
966 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b)
967 y2) z1 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_:
968 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
969 b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
970 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Appl) x x0) (THead
971 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
972 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t3 (THead (Bind
973 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
974 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
975 (_: T).(pr2 c t0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
976 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
977 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
978 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))) (sn3 c t3)
979 (\lambda (x1: B).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda
980 (x5: T).(\lambda (x6: T).(\lambda (_: (not (eq B x1 Abst))).(\lambda (H15:
981 (eq T (THead (Flat Appl) x x0) (THead (Bind x1) x2 x3))).(\lambda (H16: (eq T
982 t3 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4)))).(\lambda
983 (_: (pr2 c t0 x5)).(\lambda (_: (pr2 c x2 x6)).(\lambda (_: (pr2 (CHead c
984 (Bind x1) x6) x3 x4)).(let H20 \def (eq_ind T t3 (\lambda (t: T).((eq T
985 (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t) \to (\forall (P:
986 Prop).P))) H10 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
987 H16) in (eq_ind_r T (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5)
988 x4)) (\lambda (t: T).(sn3 c t)) (let H21 \def (eq_ind T (THead (Flat Appl) x
989 x0) (\lambda (ee: T).(match ee in T return (\lambda (_: T).Prop) with [(TSort
990 _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _)
991 \Rightarrow (match k in K return (\lambda (_: K).Prop) with [(Bind _)
992 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind x1) x2 x3)
993 H15) in (False_ind (sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O)
994 O x5) x4))) H21)) t3 H16)))))))))))))) H13)) H12)))))))))))) v2 H4))))))))) y
997 theorem sn3_appl_appls:
998 \forall (v1: T).(\forall (t1: T).(\forall (vs: TList).(let u1 \def (THeads
999 (Flat Appl) (TCons v1 vs) t1) in (\forall (c: C).((sn3 c u1) \to (\forall
1000 (v2: T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2)
1001 \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to
1002 (sn3 c (THead (Flat Appl) v2 u1))))))))))
1004 \lambda (v1: T).(\lambda (t1: T).(\lambda (vs: TList).(let u1 \def (THeads
1005 (Flat Appl) (TCons v1 vs) t1) in (\lambda (c: C).(\lambda (H: (sn3 c (THead
1006 (Flat Appl) v1 (THeads (Flat Appl) vs t1)))).(\lambda (v2: T).(\lambda (H0:
1007 (sn3 c v2)).(\lambda (H1: ((\forall (u2: T).((pr3 c (THead (Flat Appl) v1
1008 (THeads (Flat Appl) vs t1)) u2) \to ((((iso (THead (Flat Appl) v1 (THeads
1009 (Flat Appl) vs t1)) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat
1010 Appl) v2 u2))))))).(sn3_appl_appl v1 (THeads (Flat Appl) vs t1) c H v2 H0
1013 theorem sn3_appls_lref:
1014 \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (us:
1015 TList).((sns3 c us) \to (sn3 c (THeads (Flat Appl) us (TLRef i)))))))
1017 \lambda (c: C).(\lambda (i: nat).(\lambda (H: (nf2 c (TLRef i))).(\lambda
1018 (us: TList).(TList_ind (\lambda (t: TList).((sns3 c t) \to (sn3 c (THeads
1019 (Flat Appl) t (TLRef i))))) (\lambda (_: True).(sn3_nf2 c (TLRef i) H))
1020 (\lambda (t: T).(\lambda (t0: TList).(TList_ind (\lambda (t1: TList).((((sns3
1021 c t1) \to (sn3 c (THeads (Flat Appl) t1 (TLRef i))))) \to ((land (sn3 c t)
1022 (sns3 c t1)) \to (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t1 (TLRef
1023 i))))))) (\lambda (_: (((sns3 c TNil) \to (sn3 c (THeads (Flat Appl) TNil
1024 (TLRef i)))))).(\lambda (H1: (land (sn3 c t) (sns3 c TNil))).(let H2 \def H1
1025 in (and_ind (sn3 c t) True (sn3 c (THead (Flat Appl) t (THeads (Flat Appl)
1026 TNil (TLRef i)))) (\lambda (H3: (sn3 c t)).(\lambda (_: True).(sn3_appl_lref
1027 c i H t H3))) H2)))) (\lambda (t1: T).(\lambda (t2: TList).(\lambda (_:
1028 (((((sns3 c t2) \to (sn3 c (THeads (Flat Appl) t2 (TLRef i))))) \to ((land
1029 (sn3 c t) (sns3 c t2)) \to (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t2
1030 (TLRef i)))))))).(\lambda (H1: (((sns3 c (TCons t1 t2)) \to (sn3 c (THeads
1031 (Flat Appl) (TCons t1 t2) (TLRef i)))))).(\lambda (H2: (land (sn3 c t) (sns3
1032 c (TCons t1 t2)))).(let H3 \def H2 in (and_ind (sn3 c t) (land (sn3 c t1)
1033 (sns3 c t2)) (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2)
1034 (TLRef i)))) (\lambda (H4: (sn3 c t)).(\lambda (H5: (land (sn3 c t1) (sns3 c
1035 t2))).(and_ind (sn3 c t1) (sns3 c t2) (sn3 c (THead (Flat Appl) t (THeads
1036 (Flat Appl) (TCons t1 t2) (TLRef i)))) (\lambda (H6: (sn3 c t1)).(\lambda
1037 (H7: (sns3 c t2)).(sn3_appl_appls t1 (TLRef i) t2 c (H1 (conj (sn3 c t1)
1038 (sns3 c t2) H6 H7)) t H4 (\lambda (u2: T).(\lambda (H8: (pr3 c (THeads (Flat
1039 Appl) (TCons t1 t2) (TLRef i)) u2)).(\lambda (H9: (((iso (THeads (Flat Appl)
1040 (TCons t1 t2) (TLRef i)) u2) \to (\forall (P: Prop).P)))).(H9
1041 (nf2_iso_appls_lref c i H (TCons t1 t2) u2 H8) (sn3 c (THead (Flat Appl) t
1042 u2))))))))) H5))) H3))))))) t0))) us)))).
1044 theorem sn3_appls_cast:
1045 \forall (c: C).(\forall (vs: TList).(\forall (u: T).((sn3 c (THeads (Flat
1046 Appl) vs u)) \to (\forall (t: T).((sn3 c (THeads (Flat Appl) vs t)) \to (sn3
1047 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))))))))
1049 \lambda (c: C).(\lambda (vs: TList).(TList_ind (\lambda (t: TList).(\forall
1050 (u: T).((sn3 c (THeads (Flat Appl) t u)) \to (\forall (t0: T).((sn3 c (THeads
1051 (Flat Appl) t t0)) \to (sn3 c (THeads (Flat Appl) t (THead (Flat Cast) u
1052 t0)))))))) (\lambda (u: T).(\lambda (H: (sn3 c u)).(\lambda (t: T).(\lambda
1053 (H0: (sn3 c t)).(sn3_cast c u H t H0))))) (\lambda (t: T).(\lambda (t0:
1054 TList).(TList_ind (\lambda (t1: TList).(((\forall (u: T).((sn3 c (THeads
1055 (Flat Appl) t1 u)) \to (\forall (t2: T).((sn3 c (THeads (Flat Appl) t1 t2))
1056 \to (sn3 c (THeads (Flat Appl) t1 (THead (Flat Cast) u t2)))))))) \to
1057 (\forall (u: T).((sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t1 u))) \to
1058 (\forall (t2: T).((sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t1 t2)))
1059 \to (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t1 (THead (Flat Cast) u
1060 t2)))))))))) (\lambda (_: ((\forall (u: T).((sn3 c (THeads (Flat Appl) TNil
1061 u)) \to (\forall (t1: T).((sn3 c (THeads (Flat Appl) TNil t1)) \to (sn3 c
1062 (THeads (Flat Appl) TNil (THead (Flat Cast) u t1))))))))).(\lambda (u:
1063 T).(\lambda (H0: (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) TNil
1064 u)))).(\lambda (t1: T).(\lambda (H1: (sn3 c (THead (Flat Appl) t (THeads
1065 (Flat Appl) TNil t1)))).(sn3_appl_cast c t u H0 t1 H1)))))) (\lambda (t1:
1066 T).(\lambda (t2: TList).(\lambda (_: ((((\forall (u: T).((sn3 c (THeads (Flat
1067 Appl) t2 u)) \to (\forall (t3: T).((sn3 c (THeads (Flat Appl) t2 t3)) \to
1068 (sn3 c (THeads (Flat Appl) t2 (THead (Flat Cast) u t3)))))))) \to (\forall
1069 (u: T).((sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t2 u))) \to (\forall
1070 (t3: T).((sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t2 t3))) \to (sn3 c
1071 (THead (Flat Appl) t (THeads (Flat Appl) t2 (THead (Flat Cast) u
1072 t3))))))))))).(\lambda (H0: ((\forall (u: T).((sn3 c (THeads (Flat Appl)
1073 (TCons t1 t2) u)) \to (\forall (t3: T).((sn3 c (THeads (Flat Appl) (TCons t1
1074 t2) t3)) \to (sn3 c (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u
1075 t3))))))))).(\lambda (u: T).(\lambda (H1: (sn3 c (THead (Flat Appl) t (THeads
1076 (Flat Appl) (TCons t1 t2) u)))).(\lambda (t3: T).(\lambda (H2: (sn3 c (THead
1077 (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) t3)))).(let H3 \def
1078 (sn3_gen_flat Appl c t (THeads (Flat Appl) (TCons t1 t2) t3) H2) in (and_ind
1079 (sn3 c t) (sn3 c (THead (Flat Appl) t1 (THeads (Flat Appl) t2 t3))) (sn3 c
1080 (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u
1081 t3)))) (\lambda (_: (sn3 c t)).(\lambda (H5: (sn3 c (THead (Flat Appl) t1
1082 (THeads (Flat Appl) t2 t3)))).(let H6 \def H5 in (let H7 \def (sn3_gen_flat
1083 Appl c t (THeads (Flat Appl) (TCons t1 t2) u) H1) in (and_ind (sn3 c t) (sn3
1084 c (THead (Flat Appl) t1 (THeads (Flat Appl) t2 u))) (sn3 c (THead (Flat Appl)
1085 t (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)))) (\lambda (H8:
1086 (sn3 c t)).(\lambda (H9: (sn3 c (THead (Flat Appl) t1 (THeads (Flat Appl) t2
1087 u)))).(let H10 \def H9 in (sn3_appl_appls t1 (THead (Flat Cast) u t3) t2 c
1088 (H0 u H10 t3 H6) t H8 (\lambda (u2: T).(\lambda (H11: (pr3 c (THeads (Flat
1089 Appl) (TCons t1 t2) (THead (Flat Cast) u t3)) u2)).(\lambda (H12: (((iso
1090 (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u t3)) u2) \to (\forall
1091 (P: Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t (THeads (Flat Appl)
1092 (TCons t1 t2) t3)) H2 (THead (Flat Appl) t u2) (pr3_thin_dx c (THeads (Flat
1093 Appl) (TCons t1 t2) t3) u2 (pr3_iso_appls_cast c u t3 (TCons t1 t2) u2 H11
1094 H12) t Appl))))))))) H7))))) H3)))))))))) t0))) vs)).
1097 \forall (d: C).(\forall (t: T).((sn3 d t) \to (\forall (c: C).(\forall (h:
1098 nat).(\forall (i: nat).((drop h i c d) \to (sn3 c (lift h i t))))))))
1100 \lambda (d: C).(\lambda (t: T).(\lambda (H: (sn3 d t)).(sn3_ind d (\lambda
1101 (t0: T).(\forall (c: C).(\forall (h: nat).(\forall (i: nat).((drop h i c d)
1102 \to (sn3 c (lift h i t0))))))) (\lambda (t1: T).(\lambda (_: ((\forall (t2:
1103 T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 d t1 t2) \to (sn3 d
1104 t2)))))).(\lambda (H1: ((\forall (t2: T).((((eq T t1 t2) \to (\forall (P:
1105 Prop).P))) \to ((pr3 d t1 t2) \to (\forall (c: C).(\forall (h: nat).(\forall
1106 (i: nat).((drop h i c d) \to (sn3 c (lift h i t2))))))))))).(\lambda (c:
1107 C).(\lambda (h: nat).(\lambda (i: nat).(\lambda (H2: (drop h i c
1108 d)).(sn3_pr2_intro c (lift h i t1) (\lambda (t2: T).(\lambda (H3: (((eq T
1109 (lift h i t1) t2) \to (\forall (P: Prop).P)))).(\lambda (H4: (pr2 c (lift h i
1110 t1) t2)).(let H5 \def (pr2_gen_lift c t1 t2 h i H4 d H2) in (ex2_ind T
1111 (\lambda (t3: T).(eq T t2 (lift h i t3))) (\lambda (t3: T).(pr2 d t1 t3))
1112 (sn3 c t2) (\lambda (x: T).(\lambda (H6: (eq T t2 (lift h i x))).(\lambda
1113 (H7: (pr2 d t1 x)).(let H8 \def (eq_ind T t2 (\lambda (t0: T).((eq T (lift h
1114 i t1) t0) \to (\forall (P: Prop).P))) H3 (lift h i x) H6) in (eq_ind_r T
1115 (lift h i x) (\lambda (t0: T).(sn3 c t0)) (H1 x (\lambda (H9: (eq T t1
1116 x)).(\lambda (P: Prop).(let H10 \def (eq_ind_r T x (\lambda (t0: T).((eq T
1117 (lift h i t1) (lift h i t0)) \to (\forall (P0: Prop).P0))) H8 t1 H9) in (let
1118 H11 \def (eq_ind_r T x (\lambda (t0: T).(pr2 d t1 t0)) H7 t1 H9) in (H10
1119 (refl_equal T (lift h i t1)) P))))) (pr3_pr2 d t1 x H7) c h i H2) t2 H6)))))
1120 H5))))))))))))) t H))).
1123 \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
1124 (CHead d (Bind Abbr) v)) \to ((sn3 d v) \to (sn3 c (TLRef i)))))))
1126 \lambda (c: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda
1127 (H: (getl i c (CHead d (Bind Abbr) v))).(\lambda (H0: (sn3 d
1128 v)).(sn3_pr2_intro c (TLRef i) (\lambda (t2: T).(\lambda (H1: (((eq T (TLRef
1129 i) t2) \to (\forall (P: Prop).P)))).(\lambda (H2: (pr2 c (TLRef i) t2)).(let
1130 H3 \def (pr2_gen_lref c t2 i H2) in (or_ind (eq T t2 (TLRef i)) (ex2_2 C T
1131 (\lambda (d0: C).(\lambda (u: T).(getl i c (CHead d0 (Bind Abbr) u))))
1132 (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift (S i) O u))))) (sn3 c t2)
1133 (\lambda (H4: (eq T t2 (TLRef i))).(let H5 \def (eq_ind T t2 (\lambda (t:
1134 T).((eq T (TLRef i) t) \to (\forall (P: Prop).P))) H1 (TLRef i) H4) in
1135 (eq_ind_r T (TLRef i) (\lambda (t: T).(sn3 c t)) (H5 (refl_equal T (TLRef i))
1136 (sn3 c (TLRef i))) t2 H4))) (\lambda (H4: (ex2_2 C T (\lambda (d0:
1137 C).(\lambda (u: T).(getl i c (CHead d0 (Bind Abbr) u)))) (\lambda (_:
1138 C).(\lambda (u: T).(eq T t2 (lift (S i) O u)))))).(ex2_2_ind C T (\lambda
1139 (d0: C).(\lambda (u: T).(getl i c (CHead d0 (Bind Abbr) u)))) (\lambda (_:
1140 C).(\lambda (u: T).(eq T t2 (lift (S i) O u)))) (sn3 c t2) (\lambda (x0:
1141 C).(\lambda (x1: T).(\lambda (H5: (getl i c (CHead x0 (Bind Abbr)
1142 x1))).(\lambda (H6: (eq T t2 (lift (S i) O x1))).(let H7 \def (eq_ind T t2
1143 (\lambda (t: T).((eq T (TLRef i) t) \to (\forall (P: Prop).P))) H1 (lift (S
1144 i) O x1) H6) in (eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(sn3 c t)) (let
1145 H8 \def (eq_ind C (CHead d (Bind Abbr) v) (\lambda (c0: C).(getl i c c0)) H
1146 (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead d (Bind Abbr) v) i H (CHead x0
1147 (Bind Abbr) x1) H5)) in (let H9 \def (f_equal C C (\lambda (e: C).(match e in
1148 C return (\lambda (_: C).C) with [(CSort _) \Rightarrow d | (CHead c0 _ _)
1149 \Rightarrow c0])) (CHead d (Bind Abbr) v) (CHead x0 (Bind Abbr) x1)
1150 (getl_mono c (CHead d (Bind Abbr) v) i H (CHead x0 (Bind Abbr) x1) H5)) in
1151 ((let H10 \def (f_equal C T (\lambda (e: C).(match e in C return (\lambda (_:
1152 C).T) with [(CSort _) \Rightarrow v | (CHead _ _ t) \Rightarrow t])) (CHead d
1153 (Bind Abbr) v) (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead d (Bind Abbr) v)
1154 i H (CHead x0 (Bind Abbr) x1) H5)) in (\lambda (H11: (eq C d x0)).(let H12
1155 \def (eq_ind_r T x1 (\lambda (t: T).(getl i c (CHead x0 (Bind Abbr) t))) H8 v
1156 H10) in (eq_ind T v (\lambda (t: T).(sn3 c (lift (S i) O t))) (let H13 \def
1157 (eq_ind_r C x0 (\lambda (c0: C).(getl i c (CHead c0 (Bind Abbr) v))) H12 d
1158 H11) in (sn3_lift d v H0 c (S i) O (getl_drop Abbr c d v i H13))) x1 H10))))
1159 H9))) t2 H6)))))) H4)) H3))))))))))).
1162 \forall (c: C).(\forall (d: C).(\forall (h: nat).(\forall (i: nat).((drop h
1163 i c d) \to (\forall (ts: TList).((sns3 d ts) \to (sns3 c (lifts h i ts))))))))
1165 \lambda (c: C).(\lambda (d: C).(\lambda (h: nat).(\lambda (i: nat).(\lambda
1166 (H: (drop h i c d)).(\lambda (ts: TList).(TList_ind (\lambda (t:
1167 TList).((sns3 d t) \to (sns3 c (lifts h i t)))) (\lambda (H0: True).H0)
1168 (\lambda (t: T).(\lambda (t0: TList).(\lambda (H0: (((sns3 d t0) \to (sns3 c
1169 (lifts h i t0))))).(\lambda (H1: (land (sn3 d t) (sns3 d t0))).(let H2 \def
1170 H1 in (and_ind (sn3 d t) (sns3 d t0) (land (sn3 c (lift h i t)) (sns3 c
1171 (lifts h i t0))) (\lambda (H3: (sn3 d t)).(\lambda (H4: (sns3 d t0)).(conj
1172 (sn3 c (lift h i t)) (sns3 c (lifts h i t0)) (sn3_lift d t H3 c h i H) (H0
1173 H4)))) H2)))))) ts)))))).