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 include "basic_1A/sn3/nf2.ma".
19 include "basic_1A/nf2/iso.ma".
21 include "basic_1A/pr3/iso.ma".
24 \forall (c: C).(\forall (t1: T).((sn3 c t1) \to (\forall (t2: T).((pr3 c t1
25 t2) \to (sn3 c t2)))))
27 \lambda (c: C).(\lambda (t1: T).(\lambda (H: (sn3 c t1)).(sn3_ind c (\lambda
28 (t: T).(\forall (t2: T).((pr3 c t t2) \to (sn3 c t2)))) (\lambda (t2:
29 T).(\lambda (H0: ((\forall (t3: T).((((eq T t2 t3) \to (\forall (P:
30 Prop).P))) \to ((pr3 c t2 t3) \to (sn3 c t3)))))).(\lambda (H1: ((\forall
31 (t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P))) \to ((pr3 c t2 t3) \to
32 (\forall (t4: T).((pr3 c t3 t4) \to (sn3 c t4)))))))).(\lambda (t3:
33 T).(\lambda (H2: (pr3 c t2 t3)).(sn3_sing c t3 (\lambda (t0: T).(\lambda (H3:
34 (((eq T t3 t0) \to (\forall (P: Prop).P)))).(\lambda (H4: (pr3 c t3 t0)).(let
35 H_x \def (term_dec t2 t3) in (let H5 \def H_x in (or_ind (eq T t2 t3) ((eq T
36 t2 t3) \to (\forall (P: Prop).P)) (sn3 c t0) (\lambda (H6: (eq T t2 t3)).(let
37 H7 \def (eq_ind_r T t3 (\lambda (t: T).(pr3 c t t0)) H4 t2 H6) in (let H8
38 \def (eq_ind_r T t3 (\lambda (t: T).((eq T t t0) \to (\forall (P: Prop).P)))
39 H3 t2 H6) in (let H9 \def (eq_ind_r T t3 (\lambda (t: T).(pr3 c t2 t)) H2 t2
40 H6) in (H0 t0 H8 H7))))) (\lambda (H6: (((eq T t2 t3) \to (\forall (P:
41 Prop).P)))).(H1 t3 H6 H2 t0 H4)) H5)))))))))))) t1 H))).
44 \forall (c: C).(\forall (t1: T).(((\forall (t2: T).((((eq T t1 t2) \to
45 (\forall (P: Prop).P))) \to ((pr2 c t1 t2) \to (sn3 c t2))))) \to (sn3 c t1)))
47 \lambda (c: C).(\lambda (t1: T).(\lambda (H: ((\forall (t2: T).((((eq T t1
48 t2) \to (\forall (P: Prop).P))) \to ((pr2 c t1 t2) \to (sn3 c
49 t2)))))).(sn3_sing c t1 (\lambda (t2: T).(\lambda (H0: (((eq T t1 t2) \to
50 (\forall (P: Prop).P)))).(\lambda (H1: (pr3 c t1 t2)).(let H2 \def H0 in
51 ((let H3 \def H in (pr3_ind c (\lambda (t: T).(\lambda (t0: T).(((\forall
52 (t3: T).((((eq T t t3) \to (\forall (P: Prop).P))) \to ((pr2 c t t3) \to (sn3
53 c t3))))) \to ((((eq T t t0) \to (\forall (P: Prop).P))) \to (sn3 c t0)))))
54 (\lambda (t: T).(\lambda (H4: ((\forall (t3: T).((((eq T t t3) \to (\forall
55 (P: Prop).P))) \to ((pr2 c t t3) \to (sn3 c t3)))))).(\lambda (H5: (((eq T t
56 t) \to (\forall (P: Prop).P)))).(H4 t H5 (pr2_free c t t (pr0_refl t))))))
57 (\lambda (t3: T).(\lambda (t4: T).(\lambda (H4: (pr2 c t4 t3)).(\lambda (t5:
58 T).(\lambda (H5: (pr3 c t3 t5)).(\lambda (H6: ((((\forall (t6: T).((((eq T t3
59 t6) \to (\forall (P: Prop).P))) \to ((pr2 c t3 t6) \to (sn3 c t6))))) \to
60 ((((eq T t3 t5) \to (\forall (P: Prop).P))) \to (sn3 c t5))))).(\lambda (H7:
61 ((\forall (t6: T).((((eq T t4 t6) \to (\forall (P: Prop).P))) \to ((pr2 c t4
62 t6) \to (sn3 c t6)))))).(\lambda (H8: (((eq T t4 t5) \to (\forall (P:
63 Prop).P)))).(let H_x \def (term_dec t4 t3) in (let H9 \def H_x in (or_ind (eq
64 T t4 t3) ((eq T t4 t3) \to (\forall (P: Prop).P)) (sn3 c t5) (\lambda (H10:
65 (eq T t4 t3)).(let H11 \def (eq_ind T t4 (\lambda (t: T).((eq T t t5) \to
66 (\forall (P: Prop).P))) H8 t3 H10) in (let H12 \def (eq_ind T t4 (\lambda (t:
67 T).(\forall (t6: T).((((eq T t t6) \to (\forall (P: Prop).P))) \to ((pr2 c t
68 t6) \to (sn3 c t6))))) H7 t3 H10) in (let H13 \def (eq_ind T t4 (\lambda (t:
69 T).(pr2 c t t3)) H4 t3 H10) in (H6 H12 H11))))) (\lambda (H10: (((eq T t4 t3)
70 \to (\forall (P: Prop).P)))).(sn3_pr3_trans c t3 (H7 t3 H10 H4) t5 H5))
71 H9))))))))))) t1 t2 H1 H3)) H2)))))))).
74 \forall (c: C).(\forall (u: T).((sn3 c u) \to (\forall (t: T).((sn3 c t) \to
75 (sn3 c (THead (Flat Cast) u t))))))
77 \lambda (c: C).(\lambda (u: T).(\lambda (H: (sn3 c u)).(sn3_ind c (\lambda
78 (t: T).(\forall (t0: T).((sn3 c t0) \to (sn3 c (THead (Flat Cast) t t0)))))
79 (\lambda (t1: T).(\lambda (_: ((\forall (t2: T).((((eq T t1 t2) \to (\forall
80 (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c t2)))))).(\lambda (H1: ((\forall
81 (t2: T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to
82 (\forall (t: T).((sn3 c t) \to (sn3 c (THead (Flat Cast) t2
83 t))))))))).(\lambda (t: T).(\lambda (H2: (sn3 c t)).(sn3_ind c (\lambda (t0:
84 T).(sn3 c (THead (Flat Cast) t1 t0))) (\lambda (t0: T).(\lambda (H3:
85 ((\forall (t2: T).((((eq T t0 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t0
86 t2) \to (sn3 c t2)))))).(\lambda (H4: ((\forall (t2: T).((((eq T t0 t2) \to
87 (\forall (P: Prop).P))) \to ((pr3 c t0 t2) \to (sn3 c (THead (Flat Cast) t1
88 t2))))))).(sn3_pr2_intro c (THead (Flat Cast) t1 t0) (\lambda (t2:
89 T).(\lambda (H5: (((eq T (THead (Flat Cast) t1 t0) t2) \to (\forall (P:
90 Prop).P)))).(\lambda (H6: (pr2 c (THead (Flat Cast) t1 t0) t2)).(let H7 \def
91 (pr2_gen_cast c t1 t0 t2 H6) in (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda
92 (t3: T).(eq T t2 (THead (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_:
93 T).(pr2 c t1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c t0 t3)))) (pr2 c
94 t0 t2) (sn3 c t2) (\lambda (H8: (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
95 T).(eq T t2 (THead (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_:
96 T).(pr2 c t1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c t0
97 t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
98 (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c t1 u2)))
99 (\lambda (_: T).(\lambda (t3: T).(pr2 c t0 t3))) (sn3 c t2) (\lambda (x0:
100 T).(\lambda (x1: T).(\lambda (H9: (eq T t2 (THead (Flat Cast) x0
101 x1))).(\lambda (H10: (pr2 c t1 x0)).(\lambda (H11: (pr2 c t0 x1)).(let H12
102 \def (eq_ind T t2 (\lambda (t3: T).((eq T (THead (Flat Cast) t1 t0) t3) \to
103 (\forall (P: Prop).P))) H5 (THead (Flat Cast) x0 x1) H9) in (eq_ind_r T
104 (THead (Flat Cast) x0 x1) (\lambda (t3: T).(sn3 c t3)) (let H_x \def
105 (term_dec x0 t1) in (let H13 \def H_x in (or_ind (eq T x0 t1) ((eq T x0 t1)
106 \to (\forall (P: Prop).P)) (sn3 c (THead (Flat Cast) x0 x1)) (\lambda (H14:
107 (eq T x0 t1)).(let H15 \def (eq_ind T x0 (\lambda (t3: T).((eq T (THead (Flat
108 Cast) t1 t0) (THead (Flat Cast) t3 x1)) \to (\forall (P: Prop).P))) H12 t1
109 H14) in (let H16 \def (eq_ind T x0 (\lambda (t3: T).(pr2 c t1 t3)) H10 t1
110 H14) in (eq_ind_r T t1 (\lambda (t3: T).(sn3 c (THead (Flat Cast) t3 x1)))
111 (let H_x0 \def (term_dec t0 x1) in (let H17 \def H_x0 in (or_ind (eq T t0 x1)
112 ((eq T t0 x1) \to (\forall (P: Prop).P)) (sn3 c (THead (Flat Cast) t1 x1))
113 (\lambda (H18: (eq T t0 x1)).(let H19 \def (eq_ind_r T x1 (\lambda (t3:
114 T).((eq T (THead (Flat Cast) t1 t0) (THead (Flat Cast) t1 t3)) \to (\forall
115 (P: Prop).P))) H15 t0 H18) in (let H20 \def (eq_ind_r T x1 (\lambda (t3:
116 T).(pr2 c t0 t3)) H11 t0 H18) in (eq_ind T t0 (\lambda (t3: T).(sn3 c (THead
117 (Flat Cast) t1 t3))) (H19 (refl_equal T (THead (Flat Cast) t1 t0)) (sn3 c
118 (THead (Flat Cast) t1 t0))) x1 H18)))) (\lambda (H18: (((eq T t0 x1) \to
119 (\forall (P: Prop).P)))).(H4 x1 H18 (pr3_pr2 c t0 x1 H11))) H17))) x0 H14))))
120 (\lambda (H14: (((eq T x0 t1) \to (\forall (P: Prop).P)))).(H1 x0 (\lambda
121 (H15: (eq T t1 x0)).(\lambda (P: Prop).(let H16 \def (eq_ind_r T x0 (\lambda
122 (t3: T).((eq T t3 t1) \to (\forall (P0: Prop).P0))) H14 t1 H15) in (let H17
123 \def (eq_ind_r T x0 (\lambda (t3: T).((eq T (THead (Flat Cast) t1 t0) (THead
124 (Flat Cast) t3 x1)) \to (\forall (P0: Prop).P0))) H12 t1 H15) in (let H18
125 \def (eq_ind_r T x0 (\lambda (t3: T).(pr2 c t1 t3)) H10 t1 H15) in (H16
126 (refl_equal T t1) P)))))) (pr3_pr2 c t1 x0 H10) x1 (let H_x0 \def (term_dec
127 t0 x1) in (let H15 \def H_x0 in (or_ind (eq T t0 x1) ((eq T t0 x1) \to
128 (\forall (P: Prop).P)) (sn3 c x1) (\lambda (H16: (eq T t0 x1)).(let H17 \def
129 (eq_ind_r T x1 (\lambda (t3: T).((eq T (THead (Flat Cast) t1 t0) (THead (Flat
130 Cast) x0 t3)) \to (\forall (P: Prop).P))) H12 t0 H16) in (let H18 \def
131 (eq_ind_r T x1 (\lambda (t3: T).(pr2 c t0 t3)) H11 t0 H16) in (eq_ind T t0
132 (\lambda (t3: T).(sn3 c t3)) (sn3_sing c t0 H3) x1 H16)))) (\lambda (H16:
133 (((eq T t0 x1) \to (\forall (P: Prop).P)))).(H3 x1 H16 (pr3_pr2 c t0 x1
134 H11))) H15))))) H13))) t2 H9))))))) H8)) (\lambda (H8: (pr2 c t0
135 t2)).(sn3_pr3_trans c t0 (sn3_sing c t0 H3) t2 (pr3_pr2 c t0 t2 H8)))
136 H7))))))))) t H2)))))) u H))).
139 \forall (c: C).(\forall (t: T).((sn3 c t) \to (\forall (f: F).(\forall (u:
140 T).(sn3 (CHead c (Flat f) u) t)))))
142 \lambda (c: C).(\lambda (t: T).(\lambda (H: (sn3 c t)).(\lambda (f:
143 F).(\lambda (u: T).(sn3_ind c (\lambda (t0: T).(sn3 (CHead c (Flat f) u) t0))
144 (\lambda (t1: T).(\lambda (_: ((\forall (t2: T).((((eq T t1 t2) \to (\forall
145 (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c t2)))))).(\lambda (H1: ((\forall
146 (t2: T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to
147 (sn3 (CHead c (Flat f) u) t2)))))).(sn3_pr2_intro (CHead c (Flat f) u) t1
148 (\lambda (t2: T).(\lambda (H2: (((eq T t1 t2) \to (\forall (P:
149 Prop).P)))).(\lambda (H3: (pr2 (CHead c (Flat f) u) t1 t2)).(H1 t2 H2
150 (pr3_pr2 c t1 t2 (pr2_gen_cflat f c u t1 t2 H3)))))))))) t H))))).
153 \forall (b: B).(\forall (c: C).(\forall (v: T).(\forall (t: T).((sn3 c
154 (THead (Bind b) v t)) \to (sn3 (CHead c (Bind b) v) t)))))
156 \lambda (b: B).(\lambda (c: C).(\lambda (v: T).(\lambda (t: T).(\lambda (H:
157 (sn3 c (THead (Bind b) v t))).(let H_x \def (sn3_gen_bind b c v t H) in (let
158 H0 \def H_x in (land_ind (sn3 c v) (sn3 (CHead c (Bind b) v) t) (sn3 (CHead c
159 (Bind b) v) t) (\lambda (_: (sn3 c v)).(\lambda (H2: (sn3 (CHead c (Bind b)
160 v) t)).H2)) H0))))))).
163 \forall (b: B).((not (eq B b Abbr)) \to (\forall (c: C).(\forall (v1:
164 T).(\forall (t: T).((sn3 (CHead c (Bind b) v1) t) \to (\forall (v2: T).(sn3
165 (CHead c (Bind b) v2) t)))))))
167 \lambda (b: B).(\lambda (H: (not (eq B b Abbr))).(\lambda (c: C).(\lambda
168 (v1: T).(\lambda (t: T).(\lambda (H0: (sn3 (CHead c (Bind b) v1) t)).(\lambda
169 (v2: T).(sn3_ind (CHead c (Bind b) v1) (\lambda (t0: T).(sn3 (CHead c (Bind
170 b) v2) t0)) (\lambda (t1: T).(\lambda (_: ((\forall (t2: T).((((eq T t1 t2)
171 \to (\forall (P: Prop).P))) \to ((pr3 (CHead c (Bind b) v1) t1 t2) \to (sn3
172 (CHead c (Bind b) v1) t2)))))).(\lambda (H2: ((\forall (t2: T).((((eq T t1
173 t2) \to (\forall (P: Prop).P))) \to ((pr3 (CHead c (Bind b) v1) t1 t2) \to
174 (sn3 (CHead c (Bind b) v2) t2)))))).(sn3_pr2_intro (CHead c (Bind b) v2) t1
175 (\lambda (t2: T).(\lambda (H3: (((eq T t1 t2) \to (\forall (P:
176 Prop).P)))).(\lambda (H4: (pr2 (CHead c (Bind b) v2) t1 t2)).(H2 t2 H3
177 (pr3_pr2 (CHead c (Bind b) v1) t1 t2 (pr2_change b H c v2 t1 t2 H4
178 v1)))))))))) t H0))))))).
181 \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
182 (CHead d (Bind Abbr) v)) \to ((sn3 c (TLRef i)) \to (sn3 d v))))))
184 \lambda (c: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda
185 (H: (getl i c (CHead d (Bind Abbr) v))).(\lambda (H0: (sn3 c (TLRef
186 i))).(sn3_gen_lift c v (S i) O (sn3_pr3_trans c (TLRef i) H0 (lift (S i) O v)
187 (pr3_pr2 c (TLRef i) (lift (S i) O v) (pr2_delta c d v i H (TLRef i) (TLRef
188 i) (pr0_refl (TLRef i)) (lift (S i) O v) (subst0_lref v i)))) d (getl_drop
189 Abbr c d v i H))))))).
192 \forall (v: T).(\forall (t: T).(\forall (i: nat).(((\forall (w: T).(ex T
193 (\lambda (u: T).(subst0 i w t u))))) \to (\forall (c: C).(\forall (d:
194 C).((getl i c (CHead d (Bind Abbr) v)) \to ((sn3 c t) \to (sn3 d v))))))))
196 \lambda (v: T).(\lambda (t: T).(\lambda (i: nat).(\lambda (H: ((\forall (w:
197 T).(ex T (\lambda (u: T).(subst0 i w t u)))))).(let H_x \def (H v) in (let H0
198 \def H_x in (ex_ind T (\lambda (u: T).(subst0 i v t u)) (\forall (c:
199 C).(\forall (d: C).((getl i c (CHead d (Bind Abbr) v)) \to ((sn3 c t) \to
200 (sn3 d v))))) (\lambda (x: T).(\lambda (H1: (subst0 i v t x)).(subst0_ind
201 (\lambda (n: nat).(\lambda (t0: T).(\lambda (t1: T).(\lambda (_: T).(\forall
202 (c: C).(\forall (d: C).((getl n c (CHead d (Bind Abbr) t0)) \to ((sn3 c t1)
203 \to (sn3 d t0))))))))) (\lambda (v0: T).(\lambda (i0: nat).(\lambda (c:
204 C).(\lambda (d: C).(\lambda (H2: (getl i0 c (CHead d (Bind Abbr)
205 v0))).(\lambda (H3: (sn3 c (TLRef i0))).(sn3_gen_def c d v0 i0 H2 H3)))))))
206 (\lambda (v0: T).(\lambda (u2: T).(\lambda (u1: T).(\lambda (i0:
207 nat).(\lambda (_: (subst0 i0 v0 u1 u2)).(\lambda (H3: ((\forall (c:
208 C).(\forall (d: C).((getl i0 c (CHead d (Bind Abbr) v0)) \to ((sn3 c u1) \to
209 (sn3 d v0))))))).(\lambda (t0: T).(\lambda (k: K).(\lambda (c: C).(\lambda
210 (d: C).(\lambda (H4: (getl i0 c (CHead d (Bind Abbr) v0))).(\lambda (H5: (sn3
211 c (THead k u1 t0))).(let H_y \def (sn3_gen_head k c u1 t0 H5) in (H3 c d H4
212 H_y)))))))))))))) (\lambda (k: K).(\lambda (v0: T).(\lambda (t2: T).(\lambda
213 (t1: T).(\lambda (i0: nat).(\lambda (H2: (subst0 (s k i0) v0 t1 t2)).(\lambda
214 (H3: ((\forall (c: C).(\forall (d: C).((getl (s k i0) c (CHead d (Bind Abbr)
215 v0)) \to ((sn3 c t1) \to (sn3 d v0))))))).(\lambda (u: T).(\lambda (c:
216 C).(\lambda (d: C).(\lambda (H4: (getl i0 c (CHead d (Bind Abbr)
217 v0))).(\lambda (H5: (sn3 c (THead k u t1))).(K_ind (\lambda (k0: K).((subst0
218 (s k0 i0) v0 t1 t2) \to (((\forall (c0: C).(\forall (d0: C).((getl (s k0 i0)
219 c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to (sn3 d0 v0)))))) \to ((sn3
220 c (THead k0 u t1)) \to (sn3 d v0))))) (\lambda (b: B).(\lambda (_: (subst0 (s
221 (Bind b) i0) v0 t1 t2)).(\lambda (H7: ((\forall (c0: C).(\forall (d0:
222 C).((getl (s (Bind b) i0) c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to
223 (sn3 d0 v0))))))).(\lambda (H8: (sn3 c (THead (Bind b) u t1))).(let H_x0 \def
224 (sn3_gen_bind b c u t1 H8) in (let H9 \def H_x0 in (land_ind (sn3 c u) (sn3
225 (CHead c (Bind b) u) t1) (sn3 d v0) (\lambda (_: (sn3 c u)).(\lambda (H11:
226 (sn3 (CHead c (Bind b) u) t1)).(H7 (CHead c (Bind b) u) d (getl_clear_bind b
227 (CHead c (Bind b) u) c u (clear_bind b c u) (CHead d (Bind Abbr) v0) i0 H4)
228 H11))) H9))))))) (\lambda (f: F).(\lambda (_: (subst0 (s (Flat f) i0) v0 t1
229 t2)).(\lambda (H7: ((\forall (c0: C).(\forall (d0: C).((getl (s (Flat f) i0)
230 c0 (CHead d0 (Bind Abbr) v0)) \to ((sn3 c0 t1) \to (sn3 d0 v0))))))).(\lambda
231 (H8: (sn3 c (THead (Flat f) u t1))).(let H_x0 \def (sn3_gen_flat f c u t1 H8)
232 in (let H9 \def H_x0 in (land_ind (sn3 c u) (sn3 c t1) (sn3 d v0) (\lambda
233 (_: (sn3 c u)).(\lambda (H11: (sn3 c t1)).(H7 c d H4 H11))) H9))))))) k H2 H3
234 H5))))))))))))) (\lambda (v0: T).(\lambda (u1: T).(\lambda (u2: T).(\lambda
235 (i0: nat).(\lambda (_: (subst0 i0 v0 u1 u2)).(\lambda (H3: ((\forall (c:
236 C).(\forall (d: C).((getl i0 c (CHead d (Bind Abbr) v0)) \to ((sn3 c u1) \to
237 (sn3 d v0))))))).(\lambda (k: K).(\lambda (t1: T).(\lambda (t2: T).(\lambda
238 (_: (subst0 (s k i0) v0 t1 t2)).(\lambda (_: ((\forall (c: C).(\forall (d:
239 C).((getl (s k i0) c (CHead d (Bind Abbr) v0)) \to ((sn3 c t1) \to (sn3 d
240 v0))))))).(\lambda (c: C).(\lambda (d: C).(\lambda (H6: (getl i0 c (CHead d
241 (Bind Abbr) v0))).(\lambda (H7: (sn3 c (THead k u1 t1))).(let H_y \def
242 (sn3_gen_head k c u1 t1 H7) in (H3 c d H6 H_y))))))))))))))))) i v t x H1)))
245 lemma sn3_cpr3_trans:
246 \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr3 c u1 u2) \to (\forall
247 (k: K).(\forall (t: T).((sn3 (CHead c k u1) t) \to (sn3 (CHead c k u2)
250 \lambda (c: C).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pr3 c u1
251 u2)).(\lambda (k: K).(\lambda (t: T).(\lambda (H0: (sn3 (CHead c k u1)
252 t)).(sn3_ind (CHead c k u1) (\lambda (t0: T).(sn3 (CHead c k u2) t0))
253 (\lambda (t1: T).(\lambda (_: ((\forall (t2: T).((((eq T t1 t2) \to (\forall
254 (P: Prop).P))) \to ((pr3 (CHead c k u1) t1 t2) \to (sn3 (CHead c k u1)
255 t2)))))).(\lambda (H2: ((\forall (t2: T).((((eq T t1 t2) \to (\forall (P:
256 Prop).P))) \to ((pr3 (CHead c k u1) t1 t2) \to (sn3 (CHead c k u2)
257 t2)))))).(sn3_sing (CHead c k u2) t1 (\lambda (t2: T).(\lambda (H3: (((eq T
258 t1 t2) \to (\forall (P: Prop).P)))).(\lambda (H4: (pr3 (CHead c k u2) t1
259 t2)).(H2 t2 H3 (pr3_pr3_pr3_t c u1 u2 H t1 t2 k H4))))))))) t H0))))))).
262 \forall (b: B).(\forall (c: C).(\forall (u: T).((sn3 c u) \to (\forall (t:
263 T).((sn3 (CHead c (Bind b) u) t) \to (sn3 c (THead (Bind b) u t)))))))
265 \lambda (b: B).(\lambda (c: C).(\lambda (u: T).(\lambda (H: (sn3 c
266 u)).(sn3_ind c (\lambda (t: T).(\forall (t0: T).((sn3 (CHead c (Bind b) t)
267 t0) \to (sn3 c (THead (Bind b) t t0))))) (\lambda (t1: T).(\lambda (_:
268 ((\forall (t2: T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t1
269 t2) \to (sn3 c t2)))))).(\lambda (H1: ((\forall (t2: T).((((eq T t1 t2) \to
270 (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to (\forall (t: T).((sn3 (CHead c
271 (Bind b) t2) t) \to (sn3 c (THead (Bind b) t2 t))))))))).(\lambda (t:
272 T).(\lambda (H2: (sn3 (CHead c (Bind b) t1) t)).(sn3_ind (CHead c (Bind b)
273 t1) (\lambda (t0: T).(sn3 c (THead (Bind b) t1 t0))) (\lambda (t2:
274 T).(\lambda (H3: ((\forall (t3: T).((((eq T t2 t3) \to (\forall (P:
275 Prop).P))) \to ((pr3 (CHead c (Bind b) t1) t2 t3) \to (sn3 (CHead c (Bind b)
276 t1) t3)))))).(\lambda (H4: ((\forall (t3: T).((((eq T t2 t3) \to (\forall (P:
277 Prop).P))) \to ((pr3 (CHead c (Bind b) t1) t2 t3) \to (sn3 c (THead (Bind b)
278 t1 t3))))))).(sn3_sing c (THead (Bind b) t1 t2) (\lambda (t3: T).(\lambda
279 (H5: (((eq T (THead (Bind b) t1 t2) t3) \to (\forall (P: Prop).P)))).(\lambda
280 (H6: (pr3 c (THead (Bind b) t1 t2) t3)).(let H_x \def (bind_dec_not b Abst)
281 in (let H7 \def H_x in (or_ind (eq B b Abst) (not (eq B b Abst)) (sn3 c t3)
282 (\lambda (H8: (eq B b Abst)).(let H9 \def (eq_ind B b (\lambda (b0: B).(pr3 c
283 (THead (Bind b0) t1 t2) t3)) H6 Abst H8) in (let H10 \def (eq_ind B b
284 (\lambda (b0: B).((eq T (THead (Bind b0) t1 t2) t3) \to (\forall (P:
285 Prop).P))) H5 Abst H8) in (let H11 \def (eq_ind B b (\lambda (b0: B).(\forall
286 (t4: T).((((eq T t2 t4) \to (\forall (P: Prop).P))) \to ((pr3 (CHead c (Bind
287 b0) t1) t2 t4) \to (sn3 c (THead (Bind b0) t1 t4)))))) H4 Abst H8) in (let
288 H12 \def (eq_ind B b (\lambda (b0: B).(\forall (t4: T).((((eq T t2 t4) \to
289 (\forall (P: Prop).P))) \to ((pr3 (CHead c (Bind b0) t1) t2 t4) \to (sn3
290 (CHead c (Bind b0) t1) t4))))) H3 Abst H8) in (let H13 \def (eq_ind B b
291 (\lambda (b0: B).(\forall (t4: T).((((eq T t1 t4) \to (\forall (P: Prop).P)))
292 \to ((pr3 c t1 t4) \to (\forall (t0: T).((sn3 (CHead c (Bind b0) t4) t0) \to
293 (sn3 c (THead (Bind b0) t4 t0)))))))) H1 Abst H8) in (let H14 \def
294 (pr3_gen_abst c t1 t2 t3 H9) in (ex3_2_ind T T (\lambda (u2: T).(\lambda (t4:
295 T).(eq T t3 (THead (Bind Abst) u2 t4)))) (\lambda (u2: T).(\lambda (_:
296 T).(pr3 c t1 u2))) (\lambda (_: T).(\lambda (t4: T).(\forall (b0: B).(\forall
297 (u0: T).(pr3 (CHead c (Bind b0) u0) t2 t4))))) (sn3 c t3) (\lambda (x0:
298 T).(\lambda (x1: T).(\lambda (H15: (eq T t3 (THead (Bind Abst) x0
299 x1))).(\lambda (H16: (pr3 c t1 x0)).(\lambda (H17: ((\forall (b0: B).(\forall
300 (u0: T).(pr3 (CHead c (Bind b0) u0) t2 x1))))).(let H18 \def (eq_ind T t3
301 (\lambda (t0: T).((eq T (THead (Bind Abst) t1 t2) t0) \to (\forall (P:
302 Prop).P))) H10 (THead (Bind Abst) x0 x1) H15) in (eq_ind_r T (THead (Bind
303 Abst) x0 x1) (\lambda (t0: T).(sn3 c t0)) (let H_x0 \def (term_dec t1 x0) in
304 (let H19 \def H_x0 in (or_ind (eq T t1 x0) ((eq T t1 x0) \to (\forall (P:
305 Prop).P)) (sn3 c (THead (Bind Abst) x0 x1)) (\lambda (H20: (eq T t1 x0)).(let
306 H21 \def (eq_ind_r T x0 (\lambda (t0: T).((eq T (THead (Bind Abst) t1 t2)
307 (THead (Bind Abst) t0 x1)) \to (\forall (P: Prop).P))) H18 t1 H20) in (let
308 H22 \def (eq_ind_r T x0 (\lambda (t0: T).(pr3 c t1 t0)) H16 t1 H20) in
309 (eq_ind T t1 (\lambda (t0: T).(sn3 c (THead (Bind Abst) t0 x1))) (let H_x1
310 \def (term_dec t2 x1) in (let H23 \def H_x1 in (or_ind (eq T t2 x1) ((eq T t2
311 x1) \to (\forall (P: Prop).P)) (sn3 c (THead (Bind Abst) t1 x1)) (\lambda
312 (H24: (eq T t2 x1)).(let H25 \def (eq_ind_r T x1 (\lambda (t0: T).((eq T
313 (THead (Bind Abst) t1 t2) (THead (Bind Abst) t1 t0)) \to (\forall (P:
314 Prop).P))) H21 t2 H24) in (let H26 \def (eq_ind_r T x1 (\lambda (t0:
315 T).(\forall (b0: B).(\forall (u0: T).(pr3 (CHead c (Bind b0) u0) t2 t0))))
316 H17 t2 H24) in (eq_ind T t2 (\lambda (t0: T).(sn3 c (THead (Bind Abst) t1
317 t0))) (H25 (refl_equal T (THead (Bind Abst) t1 t2)) (sn3 c (THead (Bind Abst)
318 t1 t2))) x1 H24)))) (\lambda (H24: (((eq T t2 x1) \to (\forall (P:
319 Prop).P)))).(H11 x1 H24 (H17 Abst t1))) H23))) x0 H20)))) (\lambda (H20:
320 (((eq T t1 x0) \to (\forall (P: Prop).P)))).(let H_x1 \def (term_dec t2 x1)
321 in (let H21 \def H_x1 in (or_ind (eq T t2 x1) ((eq T t2 x1) \to (\forall (P:
322 Prop).P)) (sn3 c (THead (Bind Abst) x0 x1)) (\lambda (H22: (eq T t2 x1)).(let
323 H23 \def (eq_ind_r T x1 (\lambda (t0: T).(\forall (b0: B).(\forall (u0:
324 T).(pr3 (CHead c (Bind b0) u0) t2 t0)))) H17 t2 H22) in (eq_ind T t2 (\lambda
325 (t0: T).(sn3 c (THead (Bind Abst) x0 t0))) (H13 x0 H20 H16 t2 (sn3_cpr3_trans
326 c t1 x0 H16 (Bind Abst) t2 (sn3_sing (CHead c (Bind Abst) t1) t2 H12))) x1
327 H22))) (\lambda (H22: (((eq T t2 x1) \to (\forall (P: Prop).P)))).(H13 x0 H20
328 H16 x1 (sn3_cpr3_trans c t1 x0 H16 (Bind Abst) x1 (H12 x1 H22 (H17 Abst
329 t1))))) H21)))) H19))) t3 H15))))))) H14)))))))) (\lambda (H8: (not (eq B b
330 Abst))).(let H_x0 \def (pr3_gen_bind b H8 c t1 t2 t3 H6) in (let H9 \def H_x0
331 in (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind
332 b) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c t1 u2))) (\lambda (_:
333 T).(\lambda (t4: T).(pr3 (CHead c (Bind b) t1) t2 t4)))) (pr3 (CHead c (Bind
334 b) t1) t2 (lift (S O) O t3)) (sn3 c t3) (\lambda (H10: (ex3_2 T T (\lambda
335 (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind b) u2 t4)))) (\lambda (u2:
336 T).(\lambda (_: T).(pr3 c t1 u2))) (\lambda (_: T).(\lambda (t4: T).(pr3
337 (CHead c (Bind b) t1) t2 t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda
338 (t4: T).(eq T t3 (THead (Bind b) u2 t4)))) (\lambda (u2: T).(\lambda (_:
339 T).(pr3 c t1 u2))) (\lambda (_: T).(\lambda (t4: T).(pr3 (CHead c (Bind b)
340 t1) t2 t4))) (sn3 c t3) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H11: (eq
341 T t3 (THead (Bind b) x0 x1))).(\lambda (H12: (pr3 c t1 x0)).(\lambda (H13:
342 (pr3 (CHead c (Bind b) t1) t2 x1)).(let H14 \def (eq_ind T t3 (\lambda (t0:
343 T).((eq T (THead (Bind b) t1 t2) t0) \to (\forall (P: Prop).P))) H5 (THead
344 (Bind b) x0 x1) H11) in (eq_ind_r T (THead (Bind b) x0 x1) (\lambda (t0:
345 T).(sn3 c t0)) (let H_x1 \def (term_dec t1 x0) in (let H15 \def H_x1 in
346 (or_ind (eq T t1 x0) ((eq T t1 x0) \to (\forall (P: Prop).P)) (sn3 c (THead
347 (Bind b) x0 x1)) (\lambda (H16: (eq T t1 x0)).(let H17 \def (eq_ind_r T x0
348 (\lambda (t0: T).((eq T (THead (Bind b) t1 t2) (THead (Bind b) t0 x1)) \to
349 (\forall (P: Prop).P))) H14 t1 H16) in (let H18 \def (eq_ind_r T x0 (\lambda
350 (t0: T).(pr3 c t1 t0)) H12 t1 H16) in (eq_ind T t1 (\lambda (t0: T).(sn3 c
351 (THead (Bind b) t0 x1))) (let H_x2 \def (term_dec t2 x1) in (let H19 \def
352 H_x2 in (or_ind (eq T t2 x1) ((eq T t2 x1) \to (\forall (P: Prop).P)) (sn3 c
353 (THead (Bind b) t1 x1)) (\lambda (H20: (eq T t2 x1)).(let H21 \def (eq_ind_r
354 T x1 (\lambda (t0: T).((eq T (THead (Bind b) t1 t2) (THead (Bind b) t1 t0))
355 \to (\forall (P: Prop).P))) H17 t2 H20) in (let H22 \def (eq_ind_r T x1
356 (\lambda (t0: T).(pr3 (CHead c (Bind b) t1) t2 t0)) H13 t2 H20) in (eq_ind T
357 t2 (\lambda (t0: T).(sn3 c (THead (Bind b) t1 t0))) (H21 (refl_equal T (THead
358 (Bind b) t1 t2)) (sn3 c (THead (Bind b) t1 t2))) x1 H20)))) (\lambda (H20:
359 (((eq T t2 x1) \to (\forall (P: Prop).P)))).(H4 x1 H20 H13)) H19))) x0
360 H16)))) (\lambda (H16: (((eq T t1 x0) \to (\forall (P: Prop).P)))).(let H_x2
361 \def (term_dec t2 x1) in (let H17 \def H_x2 in (or_ind (eq T t2 x1) ((eq T t2
362 x1) \to (\forall (P: Prop).P)) (sn3 c (THead (Bind b) x0 x1)) (\lambda (H18:
363 (eq T t2 x1)).(let H19 \def (eq_ind_r T x1 (\lambda (t0: T).(pr3 (CHead c
364 (Bind b) t1) t2 t0)) H13 t2 H18) in (eq_ind T t2 (\lambda (t0: T).(sn3 c
365 (THead (Bind b) x0 t0))) (H1 x0 H16 H12 t2 (sn3_cpr3_trans c t1 x0 H12 (Bind
366 b) t2 (sn3_sing (CHead c (Bind b) t1) t2 H3))) x1 H18))) (\lambda (H18: (((eq
367 T t2 x1) \to (\forall (P: Prop).P)))).(H1 x0 H16 H12 x1 (sn3_cpr3_trans c t1
368 x0 H12 (Bind b) x1 (H3 x1 H18 H13)))) H17)))) H15))) t3 H11))))))) H10))
369 (\lambda (H10: (pr3 (CHead c (Bind b) t1) t2 (lift (S O) O
370 t3))).(sn3_gen_lift (CHead c (Bind b) t1) t3 (S O) O (sn3_pr3_trans (CHead c
371 (Bind b) t1) t2 (sn3_sing (CHead c (Bind b) t1) t2 H3) (lift (S O) O t3) H10)
372 c (drop_drop (Bind b) O c c (drop_refl c) t1))) H9)))) H7)))))))))) t
376 \forall (c: C).(\forall (v: T).(\forall (t: T).((sn3 c (THead (Bind Abbr) v
377 t)) \to (\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat Appl) v (THead
378 (Bind Abst) w t))))))))
380 \lambda (c: C).(\lambda (v: T).(\lambda (t: T).(\lambda (H: (sn3 c (THead
381 (Bind Abbr) v t))).(insert_eq T (THead (Bind Abbr) v t) (\lambda (t0: T).(sn3
382 c t0)) (\lambda (_: T).(\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat
383 Appl) v (THead (Bind Abst) w t)))))) (\lambda (y: T).(\lambda (H0: (sn3 c
384 y)).(unintro T t (\lambda (t0: T).((eq T y (THead (Bind Abbr) v t0)) \to
385 (\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat Appl) v (THead (Bind Abst)
386 w t0))))))) (unintro T v (\lambda (t0: T).(\forall (x: T).((eq T y (THead
387 (Bind Abbr) t0 x)) \to (\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat
388 Appl) t0 (THead (Bind Abst) w x)))))))) (sn3_ind c (\lambda (t0: T).(\forall
389 (x: T).(\forall (x0: T).((eq T t0 (THead (Bind Abbr) x x0)) \to (\forall (w:
390 T).((sn3 c w) \to (sn3 c (THead (Flat Appl) x (THead (Bind Abst) w
391 x0))))))))) (\lambda (t1: T).(\lambda (H1: ((\forall (t2: T).((((eq T t1 t2)
392 \to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c t2)))))).(\lambda
393 (H2: ((\forall (t2: T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3
394 c t1 t2) \to (\forall (x: T).(\forall (x0: T).((eq T t2 (THead (Bind Abbr) x
395 x0)) \to (\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat Appl) x (THead
396 (Bind Abst) w x0))))))))))))).(\lambda (x: T).(\lambda (x0: T).(\lambda (H3:
397 (eq T t1 (THead (Bind Abbr) x x0))).(\lambda (w: T).(\lambda (H4: (sn3 c
398 w)).(let H5 \def (eq_ind T t1 (\lambda (t0: T).(\forall (t2: T).((((eq T t0
399 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t0 t2) \to (\forall (x1:
400 T).(\forall (x2: T).((eq T t2 (THead (Bind Abbr) x1 x2)) \to (\forall (w0:
401 T).((sn3 c w0) \to (sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) w0
402 x2)))))))))))) H2 (THead (Bind Abbr) x x0) H3) in (let H6 \def (eq_ind T t1
403 (\lambda (t0: T).(\forall (t2: T).((((eq T t0 t2) \to (\forall (P: Prop).P)))
404 \to ((pr3 c t0 t2) \to (sn3 c t2))))) H1 (THead (Bind Abbr) x x0) H3) in
405 (sn3_ind c (\lambda (t0: T).(sn3 c (THead (Flat Appl) x (THead (Bind Abst) t0
406 x0)))) (\lambda (t2: T).(\lambda (H7: ((\forall (t3: T).((((eq T t2 t3) \to
407 (\forall (P: Prop).P))) \to ((pr3 c t2 t3) \to (sn3 c t3)))))).(\lambda (H8:
408 ((\forall (t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P))) \to ((pr3 c t2
409 t3) \to (sn3 c (THead (Flat Appl) x (THead (Bind Abst) t3
410 x0)))))))).(sn3_pr2_intro c (THead (Flat Appl) x (THead (Bind Abst) t2 x0))
411 (\lambda (t3: T).(\lambda (H9: (((eq T (THead (Flat Appl) x (THead (Bind
412 Abst) t2 x0)) t3) \to (\forall (P: Prop).P)))).(\lambda (H10: (pr2 c (THead
413 (Flat Appl) x (THead (Bind Abst) t2 x0)) t3)).(let H11 \def (pr2_gen_appl c x
414 (THead (Bind Abst) t2 x0) t3 H10) in (or3_ind (ex3_2 T T (\lambda (u2:
415 T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2:
416 T).(\lambda (_: T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c
417 (THead (Bind Abst) t2 x0) t4)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
418 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind Abst) t2 x0)
419 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
420 T).(\lambda (t4: T).(eq T t3 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
421 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
422 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b:
423 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4)))))))) (ex6_6 B T T T T T
424 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
425 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
426 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T
427 (THead (Bind Abst) t2 x0) (THead (Bind b) y1 z1)))))))) (\lambda (b:
428 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
429 (y2: T).(eq T t3 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2)
430 z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
431 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_:
432 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
433 (y2: T).(pr2 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
434 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b)
435 y2) z1 z2)))))))) (sn3 c t3) (\lambda (H12: (ex3_2 T T (\lambda (u2:
436 T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2:
437 T).(\lambda (_: T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c
438 (THead (Bind Abst) t2 x0) t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda
439 (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_:
440 T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c (THead (Bind Abst)
441 t2 x0) t4))) (sn3 c t3) (\lambda (x1: T).(\lambda (x2: T).(\lambda (H13: (eq
442 T t3 (THead (Flat Appl) x1 x2))).(\lambda (H14: (pr2 c x x1)).(\lambda (H15:
443 (pr2 c (THead (Bind Abst) t2 x0) x2)).(let H16 \def (eq_ind T t3 (\lambda
444 (t0: T).((eq T (THead (Flat Appl) x (THead (Bind Abst) t2 x0)) t0) \to
445 (\forall (P: Prop).P))) H9 (THead (Flat Appl) x1 x2) H13) in (eq_ind_r T
446 (THead (Flat Appl) x1 x2) (\lambda (t0: T).(sn3 c t0)) (let H17 \def
447 (pr2_gen_abst c t2 x0 x2 H15) in (ex3_2_ind T T (\lambda (u2: T).(\lambda
448 (t4: T).(eq T x2 (THead (Bind Abst) u2 t4)))) (\lambda (u2: T).(\lambda (_:
449 T).(pr2 c t2 u2))) (\lambda (_: T).(\lambda (t4: T).(\forall (b: B).(\forall
450 (u: T).(pr2 (CHead c (Bind b) u) x0 t4))))) (sn3 c (THead (Flat Appl) x1 x2))
451 (\lambda (x3: T).(\lambda (x4: T).(\lambda (H18: (eq T x2 (THead (Bind Abst)
452 x3 x4))).(\lambda (H19: (pr2 c t2 x3)).(\lambda (H20: ((\forall (b:
453 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x0 x4))))).(let H21 \def (eq_ind
454 T x2 (\lambda (t0: T).((eq T (THead (Flat Appl) x (THead (Bind Abst) t2 x0))
455 (THead (Flat Appl) x1 t0)) \to (\forall (P: Prop).P))) H16 (THead (Bind Abst)
456 x3 x4) H18) in (eq_ind_r T (THead (Bind Abst) x3 x4) (\lambda (t0: T).(sn3 c
457 (THead (Flat Appl) x1 t0))) (let H_x \def (term_dec t2 x3) in (let H22 \def
458 H_x in (or_ind (eq T t2 x3) ((eq T t2 x3) \to (\forall (P: Prop).P)) (sn3 c
459 (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))) (\lambda (H23: (eq T t2
460 x3)).(let H24 \def (eq_ind_r T x3 (\lambda (t0: T).((eq T (THead (Flat Appl)
461 x (THead (Bind Abst) t2 x0)) (THead (Flat Appl) x1 (THead (Bind Abst) t0
462 x4))) \to (\forall (P: Prop).P))) H21 t2 H23) in (let H25 \def (eq_ind_r T x3
463 (\lambda (t0: T).(pr2 c t2 t0)) H19 t2 H23) in (eq_ind T t2 (\lambda (t0:
464 T).(sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) t0 x4)))) (let H_x0 \def
465 (term_dec x x1) in (let H26 \def H_x0 in (or_ind (eq T x x1) ((eq T x x1) \to
466 (\forall (P: Prop).P)) (sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) t2
467 x4))) (\lambda (H27: (eq T x x1)).(let H28 \def (eq_ind_r T x1 (\lambda (t0:
468 T).((eq T (THead (Flat Appl) x (THead (Bind Abst) t2 x0)) (THead (Flat Appl)
469 t0 (THead (Bind Abst) t2 x4))) \to (\forall (P: Prop).P))) H24 x H27) in (let
470 H29 \def (eq_ind_r T x1 (\lambda (t0: T).(pr2 c x t0)) H14 x H27) in (eq_ind
471 T x (\lambda (t0: T).(sn3 c (THead (Flat Appl) t0 (THead (Bind Abst) t2
472 x4)))) (let H_x1 \def (term_dec x0 x4) in (let H30 \def H_x1 in (or_ind (eq T
473 x0 x4) ((eq T x0 x4) \to (\forall (P: Prop).P)) (sn3 c (THead (Flat Appl) x
474 (THead (Bind Abst) t2 x4))) (\lambda (H31: (eq T x0 x4)).(let H32 \def
475 (eq_ind_r T x4 (\lambda (t0: T).((eq T (THead (Flat Appl) x (THead (Bind
476 Abst) t2 x0)) (THead (Flat Appl) x (THead (Bind Abst) t2 t0))) \to (\forall
477 (P: Prop).P))) H28 x0 H31) in (let H33 \def (eq_ind_r T x4 (\lambda (t0:
478 T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x0 t0)))) H20 x0
479 H31) in (eq_ind T x0 (\lambda (t0: T).(sn3 c (THead (Flat Appl) x (THead
480 (Bind Abst) t2 t0)))) (H32 (refl_equal T (THead (Flat Appl) x (THead (Bind
481 Abst) t2 x0))) (sn3 c (THead (Flat Appl) x (THead (Bind Abst) t2 x0)))) x4
482 H31)))) (\lambda (H31: (((eq T x0 x4) \to (\forall (P: Prop).P)))).(H5 (THead
483 (Bind Abbr) x x4) (\lambda (H32: (eq T (THead (Bind Abbr) x x0) (THead (Bind
484 Abbr) x x4))).(\lambda (P: Prop).(let H33 \def (f_equal T T (\lambda (e:
485 T).(match e with [(TSort _) \Rightarrow x0 | (TLRef _) \Rightarrow x0 |
486 (THead _ _ t0) \Rightarrow t0])) (THead (Bind Abbr) x x0) (THead (Bind Abbr)
487 x x4) H32) in (let H34 \def (eq_ind_r T x4 (\lambda (t0: T).((eq T x0 t0) \to
488 (\forall (P0: Prop).P0))) H31 x0 H33) in (let H35 \def (eq_ind_r T x4
489 (\lambda (t0: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x0
490 t0)))) H20 x0 H33) in (H34 (refl_equal T x0) P)))))) (pr3_pr2 c (THead (Bind
491 Abbr) x x0) (THead (Bind Abbr) x x4) (pr2_head_2 c x x0 x4 (Bind Abbr) (H20
492 Abbr x))) x x4 (refl_equal T (THead (Bind Abbr) x x4)) t2 (sn3_sing c t2
493 H7))) H30))) x1 H27)))) (\lambda (H27: (((eq T x x1) \to (\forall (P:
494 Prop).P)))).(H5 (THead (Bind Abbr) x1 x4) (\lambda (H28: (eq T (THead (Bind
495 Abbr) x x0) (THead (Bind Abbr) x1 x4))).(\lambda (P: Prop).(let H29 \def
496 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow x | (TLRef
497 _) \Rightarrow x | (THead _ t0 _) \Rightarrow t0])) (THead (Bind Abbr) x x0)
498 (THead (Bind Abbr) x1 x4) H28) in ((let H30 \def (f_equal T T (\lambda (e:
499 T).(match e with [(TSort _) \Rightarrow x0 | (TLRef _) \Rightarrow x0 |
500 (THead _ _ t0) \Rightarrow t0])) (THead (Bind Abbr) x x0) (THead (Bind Abbr)
501 x1 x4) H28) in (\lambda (H31: (eq T x x1)).(let H32 \def (eq_ind_r T x4
502 (\lambda (t0: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x0
503 t0)))) H20 x0 H30) in (let H33 \def (eq_ind_r T x1 (\lambda (t0: T).((eq T x
504 t0) \to (\forall (P0: Prop).P0))) H27 x H31) in (let H34 \def (eq_ind_r T x1
505 (\lambda (t0: T).(pr2 c x t0)) H14 x H31) in (H33 (refl_equal T x) P))))))
506 H29)))) (pr3_head_12 c x x1 (pr3_pr2 c x x1 H14) (Bind Abbr) x0 x4 (pr3_pr2
507 (CHead c (Bind Abbr) x1) x0 x4 (H20 Abbr x1))) x1 x4 (refl_equal T (THead
508 (Bind Abbr) x1 x4)) t2 (sn3_sing c t2 H7))) H26))) x3 H23)))) (\lambda (H23:
509 (((eq T t2 x3) \to (\forall (P: Prop).P)))).(let H_x0 \def (term_dec x x1) in
510 (let H24 \def H_x0 in (or_ind (eq T x x1) ((eq T x x1) \to (\forall (P:
511 Prop).P)) (sn3 c (THead (Flat Appl) x1 (THead (Bind Abst) x3 x4))) (\lambda
512 (H25: (eq T x x1)).(let H26 \def (eq_ind_r T x1 (\lambda (t0: T).(pr2 c x
513 t0)) H14 x H25) in (eq_ind T x (\lambda (t0: T).(sn3 c (THead (Flat Appl) t0
514 (THead (Bind Abst) x3 x4)))) (let H_x1 \def (term_dec x0 x4) in (let H27 \def
515 H_x1 in (or_ind (eq T x0 x4) ((eq T x0 x4) \to (\forall (P: Prop).P)) (sn3 c
516 (THead (Flat Appl) x (THead (Bind Abst) x3 x4))) (\lambda (H28: (eq T x0
517 x4)).(let H29 \def (eq_ind_r T x4 (\lambda (t0: T).(\forall (b: B).(\forall
518 (u: T).(pr2 (CHead c (Bind b) u) x0 t0)))) H20 x0 H28) in (eq_ind T x0
519 (\lambda (t0: T).(sn3 c (THead (Flat Appl) x (THead (Bind Abst) x3 t0)))) (H8
520 x3 H23 (pr3_pr2 c t2 x3 H19)) x4 H28))) (\lambda (H28: (((eq T x0 x4) \to
521 (\forall (P: Prop).P)))).(H5 (THead (Bind Abbr) x x4) (\lambda (H29: (eq T
522 (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4))).(\lambda (P: Prop).(let
523 H30 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow x0
524 | (TLRef _) \Rightarrow x0 | (THead _ _ t0) \Rightarrow t0])) (THead (Bind
525 Abbr) x x0) (THead (Bind Abbr) x x4) H29) in (let H31 \def (eq_ind_r T x4
526 (\lambda (t0: T).((eq T x0 t0) \to (\forall (P0: Prop).P0))) H28 x0 H30) in
527 (let H32 \def (eq_ind_r T x4 (\lambda (t0: T).(\forall (b: B).(\forall (u:
528 T).(pr2 (CHead c (Bind b) u) x0 t0)))) H20 x0 H30) in (H31 (refl_equal T x0)
529 P)))))) (pr3_pr2 c (THead (Bind Abbr) x x0) (THead (Bind Abbr) x x4)
530 (pr2_head_2 c x x0 x4 (Bind Abbr) (H20 Abbr x))) x x4 (refl_equal T (THead
531 (Bind Abbr) x x4)) x3 (H7 x3 H23 (pr3_pr2 c t2 x3 H19)))) H27))) x1 H25)))
532 (\lambda (H25: (((eq T x x1) \to (\forall (P: Prop).P)))).(H5 (THead (Bind
533 Abbr) x1 x4) (\lambda (H26: (eq T (THead (Bind Abbr) x x0) (THead (Bind Abbr)
534 x1 x4))).(\lambda (P: Prop).(let H27 \def (f_equal T T (\lambda (e: T).(match
535 e with [(TSort _) \Rightarrow x | (TLRef _) \Rightarrow x | (THead _ t0 _)
536 \Rightarrow t0])) (THead (Bind Abbr) x x0) (THead (Bind Abbr) x1 x4) H26) in
537 ((let H28 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
538 \Rightarrow x0 | (TLRef _) \Rightarrow x0 | (THead _ _ t0) \Rightarrow t0]))
539 (THead (Bind Abbr) x x0) (THead (Bind Abbr) x1 x4) H26) in (\lambda (H29: (eq
540 T x x1)).(let H30 \def (eq_ind_r T x4 (\lambda (t0: T).(\forall (b:
541 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x0 t0)))) H20 x0 H28) in (let
542 H31 \def (eq_ind_r T x1 (\lambda (t0: T).((eq T x t0) \to (\forall (P0:
543 Prop).P0))) H25 x H29) in (let H32 \def (eq_ind_r T x1 (\lambda (t0: T).(pr2
544 c x t0)) H14 x H29) in (H31 (refl_equal T x) P)))))) H27)))) (pr3_head_12 c x
545 x1 (pr3_pr2 c x x1 H14) (Bind Abbr) x0 x4 (pr3_pr2 (CHead c (Bind Abbr) x1)
546 x0 x4 (H20 Abbr x1))) x1 x4 (refl_equal T (THead (Bind Abbr) x1 x4)) x3 (H7
547 x3 H23 (pr3_pr2 c t2 x3 H19)))) H24)))) H22))) x2 H18))))))) H17)) t3
548 H13))))))) H12)) (\lambda (H12: (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1:
549 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind Abst) t2 x0) (THead
550 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
551 T).(\lambda (t4: T).(eq T t3 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
552 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
553 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b:
554 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4))))))))).(ex4_4_ind T T T
555 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
556 (THead (Bind Abst) t2 x0) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
557 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind
558 Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
559 (_: T).(pr2 c x u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
560 T).(\lambda (t4: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
561 z1 t4))))))) (sn3 c t3) (\lambda (x1: T).(\lambda (x2: T).(\lambda (x3:
562 T).(\lambda (x4: T).(\lambda (H13: (eq T (THead (Bind Abst) t2 x0) (THead
563 (Bind Abst) x1 x2))).(\lambda (H14: (eq T t3 (THead (Bind Abbr) x3
564 x4))).(\lambda (H15: (pr2 c x x3)).(\lambda (H16: ((\forall (b: B).(\forall
565 (u: T).(pr2 (CHead c (Bind b) u) x2 x4))))).(let H17 \def (eq_ind T t3
566 (\lambda (t0: T).((eq T (THead (Flat Appl) x (THead (Bind Abst) t2 x0)) t0)
567 \to (\forall (P: Prop).P))) H9 (THead (Bind Abbr) x3 x4) H14) in (eq_ind_r T
568 (THead (Bind Abbr) x3 x4) (\lambda (t0: T).(sn3 c t0)) (let H18 \def (f_equal
569 T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t2 | (TLRef _)
570 \Rightarrow t2 | (THead _ t0 _) \Rightarrow t0])) (THead (Bind Abst) t2 x0)
571 (THead (Bind Abst) x1 x2) H13) in ((let H19 \def (f_equal T T (\lambda (e:
572 T).(match e with [(TSort _) \Rightarrow x0 | (TLRef _) \Rightarrow x0 |
573 (THead _ _ t0) \Rightarrow t0])) (THead (Bind Abst) t2 x0) (THead (Bind Abst)
574 x1 x2) H13) in (\lambda (_: (eq T t2 x1)).(let H21 \def (eq_ind_r T x2
575 (\lambda (t0: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) t0
576 x4)))) H16 x0 H19) in (let H_x \def (term_dec x x3) in (let H22 \def H_x in
577 (or_ind (eq T x x3) ((eq T x x3) \to (\forall (P: Prop).P)) (sn3 c (THead
578 (Bind Abbr) x3 x4)) (\lambda (H23: (eq T x x3)).(let H24 \def (eq_ind_r T x3
579 (\lambda (t0: T).(pr2 c x t0)) H15 x H23) in (eq_ind T x (\lambda (t0:
580 T).(sn3 c (THead (Bind Abbr) t0 x4))) (let H_x0 \def (term_dec x0 x4) in (let
581 H25 \def H_x0 in (or_ind (eq T x0 x4) ((eq T x0 x4) \to (\forall (P:
582 Prop).P)) (sn3 c (THead (Bind Abbr) x x4)) (\lambda (H26: (eq T x0 x4)).(let
583 H27 \def (eq_ind_r T x4 (\lambda (t0: T).(\forall (b: B).(\forall (u: T).(pr2
584 (CHead c (Bind b) u) x0 t0)))) H21 x0 H26) in (eq_ind T x0 (\lambda (t0:
585 T).(sn3 c (THead (Bind Abbr) x t0))) (sn3_sing c (THead (Bind Abbr) x x0) H6)
586 x4 H26))) (\lambda (H26: (((eq T x0 x4) \to (\forall (P: Prop).P)))).(H6
587 (THead (Bind Abbr) x x4) (\lambda (H27: (eq T (THead (Bind Abbr) x x0) (THead
588 (Bind Abbr) x x4))).(\lambda (P: Prop).(let H28 \def (f_equal T T (\lambda
589 (e: T).(match e with [(TSort _) \Rightarrow x0 | (TLRef _) \Rightarrow x0 |
590 (THead _ _ t0) \Rightarrow t0])) (THead (Bind Abbr) x x0) (THead (Bind Abbr)
591 x x4) H27) in (let H29 \def (eq_ind_r T x4 (\lambda (t0: T).((eq T x0 t0) \to
592 (\forall (P0: Prop).P0))) H26 x0 H28) in (let H30 \def (eq_ind_r T x4
593 (\lambda (t0: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x0
594 t0)))) H21 x0 H28) in (H29 (refl_equal T x0) P)))))) (pr3_pr2 c (THead (Bind
595 Abbr) x x0) (THead (Bind Abbr) x x4) (pr2_head_2 c x x0 x4 (Bind Abbr) (H21
596 Abbr x))))) H25))) x3 H23))) (\lambda (H23: (((eq T x x3) \to (\forall (P:
597 Prop).P)))).(H6 (THead (Bind Abbr) x3 x4) (\lambda (H24: (eq T (THead (Bind
598 Abbr) x x0) (THead (Bind Abbr) x3 x4))).(\lambda (P: Prop).(let H25 \def
599 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow x | (TLRef
600 _) \Rightarrow x | (THead _ t0 _) \Rightarrow t0])) (THead (Bind Abbr) x x0)
601 (THead (Bind Abbr) x3 x4) H24) in ((let H26 \def (f_equal T T (\lambda (e:
602 T).(match e with [(TSort _) \Rightarrow x0 | (TLRef _) \Rightarrow x0 |
603 (THead _ _ t0) \Rightarrow t0])) (THead (Bind Abbr) x x0) (THead (Bind Abbr)
604 x3 x4) H24) in (\lambda (H27: (eq T x x3)).(let H28 \def (eq_ind_r T x4
605 (\lambda (t0: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x0
606 t0)))) H21 x0 H26) in (let H29 \def (eq_ind_r T x3 (\lambda (t0: T).((eq T x
607 t0) \to (\forall (P0: Prop).P0))) H23 x H27) in (let H30 \def (eq_ind_r T x3
608 (\lambda (t0: T).(pr2 c x t0)) H15 x H27) in (H29 (refl_equal T x) P))))))
609 H25)))) (pr3_head_12 c x x3 (pr3_pr2 c x x3 H15) (Bind Abbr) x0 x4 (pr3_pr2
610 (CHead c (Bind Abbr) x3) x0 x4 (H21 Abbr x3))))) H22)))))) H18)) t3
611 H14)))))))))) H12)) (\lambda (H12: (ex6_6 B T T T T T (\lambda (b:
612 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
613 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
614 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind
615 Abst) t2 x0) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
616 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
617 t3 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
618 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
619 T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1:
620 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
621 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
622 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1
623 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda
624 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b
625 Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
626 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind Abst) t2 x0) (THead
627 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
628 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t3 (THead (Bind
629 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
630 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
631 (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
632 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
633 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
634 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))) (sn3 c t3)
635 (\lambda (x1: B).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda
636 (x5: T).(\lambda (x6: T).(\lambda (H13: (not (eq B x1 Abst))).(\lambda (H14:
637 (eq T (THead (Bind Abst) t2 x0) (THead (Bind x1) x2 x3))).(\lambda (H15: (eq
638 T t3 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4)))).(\lambda
639 (_: (pr2 c x x5)).(\lambda (H17: (pr2 c x2 x6)).(\lambda (H18: (pr2 (CHead c
640 (Bind x1) x6) x3 x4)).(let H19 \def (eq_ind T t3 (\lambda (t0: T).((eq T
641 (THead (Flat Appl) x (THead (Bind Abst) t2 x0)) t0) \to (\forall (P:
642 Prop).P))) H9 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
643 H15) in (eq_ind_r T (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5)
644 x4)) (\lambda (t0: T).(sn3 c t0)) (let H20 \def (f_equal T B (\lambda (e:
645 T).(match e with [(TSort _) \Rightarrow Abst | (TLRef _) \Rightarrow Abst |
646 (THead k _ _) \Rightarrow (match k with [(Bind b) \Rightarrow b | (Flat _)
647 \Rightarrow Abst])])) (THead (Bind Abst) t2 x0) (THead (Bind x1) x2 x3) H14)
648 in ((let H21 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
649 \Rightarrow t2 | (TLRef _) \Rightarrow t2 | (THead _ t0 _) \Rightarrow t0]))
650 (THead (Bind Abst) t2 x0) (THead (Bind x1) x2 x3) H14) in ((let H22 \def
651 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow x0 | (TLRef
652 _) \Rightarrow x0 | (THead _ _ t0) \Rightarrow t0])) (THead (Bind Abst) t2
653 x0) (THead (Bind x1) x2 x3) H14) in (\lambda (H23: (eq T t2 x2)).(\lambda
654 (H24: (eq B Abst x1)).(let H25 \def (eq_ind_r T x3 (\lambda (t0: T).(pr2
655 (CHead c (Bind x1) x6) t0 x4)) H18 x0 H22) in (let H26 \def (eq_ind_r T x2
656 (\lambda (t0: T).(pr2 c t0 x6)) H17 t2 H23) in (let H27 \def (eq_ind_r B x1
657 (\lambda (b: B).(pr2 (CHead c (Bind b) x6) x0 x4)) H25 Abst H24) in (let H28
658 \def (eq_ind_r B x1 (\lambda (b: B).(not (eq B b Abst))) H13 Abst H24) in
659 (eq_ind B Abst (\lambda (b: B).(sn3 c (THead (Bind b) x6 (THead (Flat Appl)
660 (lift (S O) O x5) x4)))) (let H29 \def (match (H28 (refl_equal B Abst)) in
661 False with []) in H29) x1 H24)))))))) H21)) H20)) t3 H15)))))))))))))) H12))
662 H11))))))))) w H4))))))))))) y H0))))) H)))).
665 \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (v:
666 T).((sn3 c v) \to (sn3 c (THead (Flat Appl) v (TLRef i)))))))
668 \lambda (c: C).(\lambda (i: nat).(\lambda (H: (nf2 c (TLRef i))).(\lambda
669 (v: T).(\lambda (H0: (sn3 c v)).(sn3_ind c (\lambda (t: T).(sn3 c (THead
670 (Flat Appl) t (TLRef i)))) (\lambda (t1: T).(\lambda (_: ((\forall (t2:
671 T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c
672 t2)))))).(\lambda (H2: ((\forall (t2: T).((((eq T t1 t2) \to (\forall (P:
673 Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c (THead (Flat Appl) t2 (TLRef
674 i)))))))).(sn3_pr2_intro c (THead (Flat Appl) t1 (TLRef i)) (\lambda (t2:
675 T).(\lambda (H3: (((eq T (THead (Flat Appl) t1 (TLRef i)) t2) \to (\forall
676 (P: Prop).P)))).(\lambda (H4: (pr2 c (THead (Flat Appl) t1 (TLRef i))
677 t2)).(let H5 \def (pr2_gen_appl c t1 (TLRef i) t2 H4) in (or3_ind (ex3_2 T T
678 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
679 (\lambda (u2: T).(\lambda (_: T).(pr2 c t1 u2))) (\lambda (_: T).(\lambda
680 (t3: T).(pr2 c (TLRef i) t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1:
681 T).(\lambda (_: T).(\lambda (_: T).(eq T (TLRef i) (THead (Bind Abst) y1
682 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3:
683 T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_:
684 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t1 u2))))) (\lambda (_:
685 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall
686 (u: T).(pr2 (CHead c (Bind b) u) z1 t3)))))))) (ex6_6 B T T T T T (\lambda
687 (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
688 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
689 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T
690 (TLRef i) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
691 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
692 t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
693 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
694 T).(\lambda (_: T).(pr2 c t1 u2))))))) (\lambda (_: B).(\lambda (y1:
695 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
696 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
697 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))))
698 (sn3 c t2) (\lambda (H6: (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T
699 t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c t1
700 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c (TLRef i) t3))))).(ex3_2_ind T
701 T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
702 (\lambda (u2: T).(\lambda (_: T).(pr2 c t1 u2))) (\lambda (_: T).(\lambda
703 (t3: T).(pr2 c (TLRef i) t3))) (sn3 c t2) (\lambda (x0: T).(\lambda (x1:
704 T).(\lambda (H7: (eq T t2 (THead (Flat Appl) x0 x1))).(\lambda (H8: (pr2 c t1
705 x0)).(\lambda (H9: (pr2 c (TLRef i) x1)).(let H10 \def (eq_ind T t2 (\lambda
706 (t: T).((eq T (THead (Flat Appl) t1 (TLRef i)) t) \to (\forall (P: Prop).P)))
707 H3 (THead (Flat Appl) x0 x1) H7) in (eq_ind_r T (THead (Flat Appl) x0 x1)
708 (\lambda (t: T).(sn3 c t)) (let H11 \def (eq_ind_r T x1 (\lambda (t: T).((eq
709 T (THead (Flat Appl) t1 (TLRef i)) (THead (Flat Appl) x0 t)) \to (\forall (P:
710 Prop).P))) H10 (TLRef i) (H x1 H9)) in (let H12 \def (eq_ind_r T x1 (\lambda
711 (t: T).(pr2 c (TLRef i) t)) H9 (TLRef i) (H x1 H9)) in (eq_ind T (TLRef i)
712 (\lambda (t: T).(sn3 c (THead (Flat Appl) x0 t))) (let H_x \def (term_dec t1
713 x0) in (let H13 \def H_x in (or_ind (eq T t1 x0) ((eq T t1 x0) \to (\forall
714 (P: Prop).P)) (sn3 c (THead (Flat Appl) x0 (TLRef i))) (\lambda (H14: (eq T
715 t1 x0)).(let H15 \def (eq_ind_r T x0 (\lambda (t: T).((eq T (THead (Flat
716 Appl) t1 (TLRef i)) (THead (Flat Appl) t (TLRef i))) \to (\forall (P:
717 Prop).P))) H11 t1 H14) in (let H16 \def (eq_ind_r T x0 (\lambda (t: T).(pr2 c
718 t1 t)) H8 t1 H14) in (eq_ind T t1 (\lambda (t: T).(sn3 c (THead (Flat Appl) t
719 (TLRef i)))) (H15 (refl_equal T (THead (Flat Appl) t1 (TLRef i))) (sn3 c
720 (THead (Flat Appl) t1 (TLRef i)))) x0 H14)))) (\lambda (H14: (((eq T t1 x0)
721 \to (\forall (P: Prop).P)))).(H2 x0 H14 (pr3_pr2 c t1 x0 H8))) H13))) x1 (H
722 x1 H9)))) t2 H7))))))) H6)) (\lambda (H6: (ex4_4 T T T T (\lambda (y1:
723 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (TLRef i) (THead
724 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
725 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
726 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t1 u2)))))
727 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall
728 (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t3))))))))).(ex4_4_ind T
729 T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
730 (TLRef i) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_:
731 T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3))))))
732 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t1
733 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3:
734 T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t3)))))))
735 (sn3 c t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3:
736 T).(\lambda (H7: (eq T (TLRef i) (THead (Bind Abst) x0 x1))).(\lambda (H8:
737 (eq T t2 (THead (Bind Abbr) x2 x3))).(\lambda (_: (pr2 c t1 x2)).(\lambda (_:
738 ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x1 x3))))).(let
739 H11 \def (eq_ind T t2 (\lambda (t: T).((eq T (THead (Flat Appl) t1 (TLRef i))
740 t) \to (\forall (P: Prop).P))) H3 (THead (Bind Abbr) x2 x3) H8) in (eq_ind_r
741 T (THead (Bind Abbr) x2 x3) (\lambda (t: T).(sn3 c t)) (let H12 \def (eq_ind
742 T (TLRef i) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
743 (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead
744 (Bind Abst) x0 x1) H7) in (False_ind (sn3 c (THead (Bind Abbr) x2 x3)) H12))
745 t2 H8)))))))))) H6)) (\lambda (H6: (ex6_6 B T T T T T (\lambda (b:
746 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
747 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
748 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (TLRef i)
749 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
750 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
751 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
752 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
753 (_: T).(pr2 c t1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
754 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
755 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
756 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))))).(ex6_6_ind
757 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
758 T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
759 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
760 (_: T).(eq T (TLRef i) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda
761 (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq
762 T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
763 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
764 T).(\lambda (_: T).(pr2 c t1 u2))))))) (\lambda (_: B).(\lambda (y1:
765 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
766 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
767 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))
768 (sn3 c t2) (\lambda (x0: B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3:
769 T).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: (not (eq B x0
770 Abst))).(\lambda (H8: (eq T (TLRef i) (THead (Bind x0) x1 x2))).(\lambda (H9:
771 (eq T t2 (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4)
772 x3)))).(\lambda (_: (pr2 c t1 x4)).(\lambda (_: (pr2 c x1 x5)).(\lambda (_:
773 (pr2 (CHead c (Bind x0) x5) x2 x3)).(let H13 \def (eq_ind T t2 (\lambda (t:
774 T).((eq T (THead (Flat Appl) t1 (TLRef i)) t) \to (\forall (P: Prop).P))) H3
775 (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)) H9) in
776 (eq_ind_r T (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))
777 (\lambda (t: T).(sn3 c t)) (let H14 \def (eq_ind T (TLRef i) (\lambda (ee:
778 T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
779 (THead _ _ _) \Rightarrow False])) I (THead (Bind x0) x1 x2) H8) in
780 (False_ind (sn3 c (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4)
781 x3))) H14)) t2 H9)))))))))))))) H6)) H5))))))))) v H0))))).
784 \forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c
785 (CHead d (Bind Abbr) w)) \to (\forall (v: T).((sn3 c (THead (Flat Appl) v
786 (lift (S i) O w))) \to (sn3 c (THead (Flat Appl) v (TLRef i)))))))))
788 \lambda (c: C).(\lambda (d: C).(\lambda (w: T).(\lambda (i: nat).(\lambda
789 (H: (getl i c (CHead d (Bind Abbr) w))).(\lambda (v: T).(\lambda (H0: (sn3 c
790 (THead (Flat Appl) v (lift (S i) O w)))).(insert_eq T (THead (Flat Appl) v
791 (lift (S i) O w)) (\lambda (t: T).(sn3 c t)) (\lambda (_: T).(sn3 c (THead
792 (Flat Appl) v (TLRef i)))) (\lambda (y: T).(\lambda (H1: (sn3 c y)).(unintro
793 T v (\lambda (t: T).((eq T y (THead (Flat Appl) t (lift (S i) O w))) \to (sn3
794 c (THead (Flat Appl) t (TLRef i))))) (sn3_ind c (\lambda (t: T).(\forall (x:
795 T).((eq T t (THead (Flat Appl) x (lift (S i) O w))) \to (sn3 c (THead (Flat
796 Appl) x (TLRef i)))))) (\lambda (t1: T).(\lambda (H2: ((\forall (t2:
797 T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c
798 t2)))))).(\lambda (H3: ((\forall (t2: T).((((eq T t1 t2) \to (\forall (P:
799 Prop).P))) \to ((pr3 c t1 t2) \to (\forall (x: T).((eq T t2 (THead (Flat
800 Appl) x (lift (S i) O w))) \to (sn3 c (THead (Flat Appl) x (TLRef
801 i)))))))))).(\lambda (x: T).(\lambda (H4: (eq T t1 (THead (Flat Appl) x (lift
802 (S i) O w)))).(let H5 \def (eq_ind T t1 (\lambda (t: T).(\forall (t2:
803 T).((((eq T t t2) \to (\forall (P: Prop).P))) \to ((pr3 c t t2) \to (\forall
804 (x0: T).((eq T t2 (THead (Flat Appl) x0 (lift (S i) O w))) \to (sn3 c (THead
805 (Flat Appl) x0 (TLRef i))))))))) H3 (THead (Flat Appl) x (lift (S i) O w))
806 H4) in (let H6 \def (eq_ind T t1 (\lambda (t: T).(\forall (t2: T).((((eq T t
807 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t t2) \to (sn3 c t2))))) H2
808 (THead (Flat Appl) x (lift (S i) O w)) H4) in (sn3_pr2_intro c (THead (Flat
809 Appl) x (TLRef i)) (\lambda (t2: T).(\lambda (H7: (((eq T (THead (Flat Appl)
810 x (TLRef i)) t2) \to (\forall (P: Prop).P)))).(\lambda (H8: (pr2 c (THead
811 (Flat Appl) x (TLRef i)) t2)).(let H9 \def (pr2_gen_appl c x (TLRef i) t2 H8)
812 in (or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
813 (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
814 (\lambda (_: T).(\lambda (t3: T).(pr2 c (TLRef i) t3)))) (ex4_4 T T T T
815 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
816 (TLRef i) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_:
817 T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3))))))
818 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x
819 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3:
820 T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t3))))))))
821 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
822 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
823 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
824 (_: T).(eq T (TLRef i) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda
825 (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq
826 T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
827 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
828 T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1:
829 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
830 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
831 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))))
832 (sn3 c t2) (\lambda (H10: (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T
833 t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x
834 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c (TLRef i) t3))))).(ex3_2_ind T
835 T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3))))
836 (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t3:
837 T).(pr2 c (TLRef i) t3))) (sn3 c t2) (\lambda (x0: T).(\lambda (x1:
838 T).(\lambda (H11: (eq T t2 (THead (Flat Appl) x0 x1))).(\lambda (H12: (pr2 c
839 x x0)).(\lambda (H13: (pr2 c (TLRef i) x1)).(let H14 \def (eq_ind T t2
840 (\lambda (t: T).((eq T (THead (Flat Appl) x (TLRef i)) t) \to (\forall (P:
841 Prop).P))) H7 (THead (Flat Appl) x0 x1) H11) in (eq_ind_r T (THead (Flat
842 Appl) x0 x1) (\lambda (t: T).(sn3 c t)) (let H15 \def (pr2_gen_lref c x1 i
843 H13) in (or_ind (eq T x1 (TLRef i)) (ex2_2 C T (\lambda (d0: C).(\lambda (u:
844 T).(getl i c (CHead d0 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq
845 T x1 (lift (S i) O u))))) (sn3 c (THead (Flat Appl) x0 x1)) (\lambda (H16:
846 (eq T x1 (TLRef i))).(let H17 \def (eq_ind T x1 (\lambda (t: T).((eq T (THead
847 (Flat Appl) x (TLRef i)) (THead (Flat Appl) x0 t)) \to (\forall (P:
848 Prop).P))) H14 (TLRef i) H16) in (eq_ind_r T (TLRef i) (\lambda (t: T).(sn3 c
849 (THead (Flat Appl) x0 t))) (let H_x \def (term_dec x x0) in (let H18 \def H_x
850 in (or_ind (eq T x x0) ((eq T x x0) \to (\forall (P: Prop).P)) (sn3 c (THead
851 (Flat Appl) x0 (TLRef i))) (\lambda (H19: (eq T x x0)).(let H20 \def
852 (eq_ind_r T x0 (\lambda (t: T).((eq T (THead (Flat Appl) x (TLRef i)) (THead
853 (Flat Appl) t (TLRef i))) \to (\forall (P: Prop).P))) H17 x H19) in (let H21
854 \def (eq_ind_r T x0 (\lambda (t: T).(pr2 c x t)) H12 x H19) in (eq_ind T x
855 (\lambda (t: T).(sn3 c (THead (Flat Appl) t (TLRef i)))) (H20 (refl_equal T
856 (THead (Flat Appl) x (TLRef i))) (sn3 c (THead (Flat Appl) x (TLRef i)))) x0
857 H19)))) (\lambda (H19: (((eq T x x0) \to (\forall (P: Prop).P)))).(H5 (THead
858 (Flat Appl) x0 (lift (S i) O w)) (\lambda (H20: (eq T (THead (Flat Appl) x
859 (lift (S i) O w)) (THead (Flat Appl) x0 (lift (S i) O w)))).(\lambda (P:
860 Prop).(let H21 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
861 \Rightarrow x | (TLRef _) \Rightarrow x | (THead _ t _) \Rightarrow t]))
862 (THead (Flat Appl) x (lift (S i) O w)) (THead (Flat Appl) x0 (lift (S i) O
863 w)) H20) in (let H22 \def (eq_ind_r T x0 (\lambda (t: T).((eq T x t) \to
864 (\forall (P0: Prop).P0))) H19 x H21) in (let H23 \def (eq_ind_r T x0 (\lambda
865 (t: T).(pr2 c x t)) H12 x H21) in (H22 (refl_equal T x) P)))))) (pr3_pr2 c
866 (THead (Flat Appl) x (lift (S i) O w)) (THead (Flat Appl) x0 (lift (S i) O
867 w)) (pr2_head_1 c x x0 H12 (Flat Appl) (lift (S i) O w))) x0 (refl_equal T
868 (THead (Flat Appl) x0 (lift (S i) O w))))) H18))) x1 H16))) (\lambda (H16:
869 (ex2_2 C T (\lambda (d0: C).(\lambda (u: T).(getl i c (CHead d0 (Bind Abbr)
870 u)))) (\lambda (_: C).(\lambda (u: T).(eq T x1 (lift (S i) O
871 u)))))).(ex2_2_ind C T (\lambda (d0: C).(\lambda (u: T).(getl i c (CHead d0
872 (Bind Abbr) u)))) (\lambda (_: C).(\lambda (u: T).(eq T x1 (lift (S i) O
873 u)))) (sn3 c (THead (Flat Appl) x0 x1)) (\lambda (x2: C).(\lambda (x3:
874 T).(\lambda (H17: (getl i c (CHead x2 (Bind Abbr) x3))).(\lambda (H18: (eq T
875 x1 (lift (S i) O x3))).(let H19 \def (eq_ind T x1 (\lambda (t: T).((eq T
876 (THead (Flat Appl) x (TLRef i)) (THead (Flat Appl) x0 t)) \to (\forall (P:
877 Prop).P))) H14 (lift (S i) O x3) H18) in (eq_ind_r T (lift (S i) O x3)
878 (\lambda (t: T).(sn3 c (THead (Flat Appl) x0 t))) (let H20 \def (eq_ind C
879 (CHead d (Bind Abbr) w) (\lambda (c0: C).(getl i c c0)) H (CHead x2 (Bind
880 Abbr) x3) (getl_mono c (CHead d (Bind Abbr) w) i H (CHead x2 (Bind Abbr) x3)
881 H17)) in (let H21 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
882 \Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d (Bind Abbr) w)
883 (CHead x2 (Bind Abbr) x3) (getl_mono c (CHead d (Bind Abbr) w) i H (CHead x2
884 (Bind Abbr) x3) H17)) in ((let H22 \def (f_equal C T (\lambda (e: C).(match e
885 with [(CSort _) \Rightarrow w | (CHead _ _ t) \Rightarrow t])) (CHead d (Bind
886 Abbr) w) (CHead x2 (Bind Abbr) x3) (getl_mono c (CHead d (Bind Abbr) w) i H
887 (CHead x2 (Bind Abbr) x3) H17)) in (\lambda (H23: (eq C d x2)).(let H24 \def
888 (eq_ind_r T x3 (\lambda (t: T).(getl i c (CHead x2 (Bind Abbr) t))) H20 w
889 H22) in (eq_ind T w (\lambda (t: T).(sn3 c (THead (Flat Appl) x0 (lift (S i)
890 O t)))) (let H25 \def (eq_ind_r C x2 (\lambda (c0: C).(getl i c (CHead c0
891 (Bind Abbr) w))) H24 d H23) in (let H_x \def (term_dec x x0) in (let H26 \def
892 H_x in (or_ind (eq T x x0) ((eq T x x0) \to (\forall (P: Prop).P)) (sn3 c
893 (THead (Flat Appl) x0 (lift (S i) O w))) (\lambda (H27: (eq T x x0)).(let H28
894 \def (eq_ind_r T x0 (\lambda (t: T).(pr2 c x t)) H12 x H27) in (eq_ind T x
895 (\lambda (t: T).(sn3 c (THead (Flat Appl) t (lift (S i) O w)))) (sn3_sing c
896 (THead (Flat Appl) x (lift (S i) O w)) H6) x0 H27))) (\lambda (H27: (((eq T x
897 x0) \to (\forall (P: Prop).P)))).(H6 (THead (Flat Appl) x0 (lift (S i) O w))
898 (\lambda (H28: (eq T (THead (Flat Appl) x (lift (S i) O w)) (THead (Flat
899 Appl) x0 (lift (S i) O w)))).(\lambda (P: Prop).(let H29 \def (f_equal T T
900 (\lambda (e: T).(match e with [(TSort _) \Rightarrow x | (TLRef _)
901 \Rightarrow x | (THead _ t _) \Rightarrow t])) (THead (Flat Appl) x (lift (S
902 i) O w)) (THead (Flat Appl) x0 (lift (S i) O w)) H28) in (let H30 \def
903 (eq_ind_r T x0 (\lambda (t: T).((eq T x t) \to (\forall (P0: Prop).P0))) H27
904 x H29) in (let H31 \def (eq_ind_r T x0 (\lambda (t: T).(pr2 c x t)) H12 x
905 H29) in (H30 (refl_equal T x) P)))))) (pr3_pr2 c (THead (Flat Appl) x (lift
906 (S i) O w)) (THead (Flat Appl) x0 (lift (S i) O w)) (pr2_head_1 c x x0 H12
907 (Flat Appl) (lift (S i) O w))))) H26)))) x3 H22)))) H21))) x1 H18)))))) H16))
908 H15)) t2 H11))))))) H10)) (\lambda (H10: (ex4_4 T T T T (\lambda (y1:
909 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (TLRef i) (THead
910 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
911 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
912 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
913 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b:
914 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t3))))))))).(ex4_4_ind T T T
915 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
916 (TLRef i) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_:
917 T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3))))))
918 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x
919 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3:
920 T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t3)))))))
921 (sn3 c t2) (\lambda (x0: T).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3:
922 T).(\lambda (H11: (eq T (TLRef i) (THead (Bind Abst) x0 x1))).(\lambda (H12:
923 (eq T t2 (THead (Bind Abbr) x2 x3))).(\lambda (_: (pr2 c x x2)).(\lambda (_:
924 ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x1 x3))))).(let
925 H15 \def (eq_ind T t2 (\lambda (t: T).((eq T (THead (Flat Appl) x (TLRef i))
926 t) \to (\forall (P: Prop).P))) H7 (THead (Bind Abbr) x2 x3) H12) in (eq_ind_r
927 T (THead (Bind Abbr) x2 x3) (\lambda (t: T).(sn3 c t)) (let H16 \def (eq_ind
928 T (TLRef i) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
929 (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I (THead
930 (Bind Abst) x0 x1) H11) in (False_ind (sn3 c (THead (Bind Abbr) x2 x3)) H16))
931 t2 H12)))))))))) H10)) (\lambda (H10: (ex6_6 B T T T T T (\lambda (b:
932 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
933 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
934 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (TLRef i)
935 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
936 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
937 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
938 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
939 (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
940 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
941 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
942 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))))).(ex6_6_ind
943 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
944 T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
945 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
946 (_: T).(eq T (TLRef i) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda
947 (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq
948 T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
949 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
950 T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1:
951 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
952 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
953 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))
954 (sn3 c t2) (\lambda (x0: B).(\lambda (x1: T).(\lambda (x2: T).(\lambda (x3:
955 T).(\lambda (x4: T).(\lambda (x5: T).(\lambda (_: (not (eq B x0
956 Abst))).(\lambda (H12: (eq T (TLRef i) (THead (Bind x0) x1 x2))).(\lambda
957 (H13: (eq T t2 (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4)
958 x3)))).(\lambda (_: (pr2 c x x4)).(\lambda (_: (pr2 c x1 x5)).(\lambda (_:
959 (pr2 (CHead c (Bind x0) x5) x2 x3)).(let H17 \def (eq_ind T t2 (\lambda (t:
960 T).((eq T (THead (Flat Appl) x (TLRef i)) t) \to (\forall (P: Prop).P))) H7
961 (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3)) H13) in
962 (eq_ind_r T (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4) x3))
963 (\lambda (t: T).(sn3 c t)) (let H18 \def (eq_ind T (TLRef i) (\lambda (ee:
964 T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
965 (THead _ _ _) \Rightarrow False])) I (THead (Bind x0) x1 x2) H12) in
966 (False_ind (sn3 c (THead (Bind x0) x5 (THead (Flat Appl) (lift (S O) O x4)
967 x3))) H18)) t2 H13)))))))))))))) H10)) H9))))))))))))) y H1)))) H0))))))).
969 theorem sn3_appl_cast:
970 \forall (c: C).(\forall (v: T).(\forall (u: T).((sn3 c (THead (Flat Appl) v
971 u)) \to (\forall (t: T).((sn3 c (THead (Flat Appl) v t)) \to (sn3 c (THead
972 (Flat Appl) v (THead (Flat Cast) u t))))))))
974 \lambda (c: C).(\lambda (v: T).(\lambda (u: T).(\lambda (H: (sn3 c (THead
975 (Flat Appl) v u))).(insert_eq T (THead (Flat Appl) v u) (\lambda (t: T).(sn3
976 c t)) (\lambda (_: T).(\forall (t0: T).((sn3 c (THead (Flat Appl) v t0)) \to
977 (sn3 c (THead (Flat Appl) v (THead (Flat Cast) u t0)))))) (\lambda (y:
978 T).(\lambda (H0: (sn3 c y)).(unintro T u (\lambda (t: T).((eq T y (THead
979 (Flat Appl) v t)) \to (\forall (t0: T).((sn3 c (THead (Flat Appl) v t0)) \to
980 (sn3 c (THead (Flat Appl) v (THead (Flat Cast) t t0))))))) (unintro T v
981 (\lambda (t: T).(\forall (x: T).((eq T y (THead (Flat Appl) t x)) \to
982 (\forall (t0: T).((sn3 c (THead (Flat Appl) t t0)) \to (sn3 c (THead (Flat
983 Appl) t (THead (Flat Cast) x t0)))))))) (sn3_ind c (\lambda (t: T).(\forall
984 (x: T).(\forall (x0: T).((eq T t (THead (Flat Appl) x x0)) \to (\forall (t0:
985 T).((sn3 c (THead (Flat Appl) x t0)) \to (sn3 c (THead (Flat Appl) x (THead
986 (Flat Cast) x0 t0))))))))) (\lambda (t1: T).(\lambda (H1: ((\forall (t2:
987 T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c
988 t2)))))).(\lambda (H2: ((\forall (t2: T).((((eq T t1 t2) \to (\forall (P:
989 Prop).P))) \to ((pr3 c t1 t2) \to (\forall (x: T).(\forall (x0: T).((eq T t2
990 (THead (Flat Appl) x x0)) \to (\forall (t: T).((sn3 c (THead (Flat Appl) x
991 t)) \to (sn3 c (THead (Flat Appl) x (THead (Flat Cast) x0
992 t))))))))))))).(\lambda (x: T).(\lambda (x0: T).(\lambda (H3: (eq T t1 (THead
993 (Flat Appl) x x0))).(\lambda (t: T).(\lambda (H4: (sn3 c (THead (Flat Appl) x
994 t))).(insert_eq T (THead (Flat Appl) x t) (\lambda (t0: T).(sn3 c t0))
995 (\lambda (_: T).(sn3 c (THead (Flat Appl) x (THead (Flat Cast) x0 t))))
996 (\lambda (y0: T).(\lambda (H5: (sn3 c y0)).(unintro T t (\lambda (t0: T).((eq
997 T y0 (THead (Flat Appl) x t0)) \to (sn3 c (THead (Flat Appl) x (THead (Flat
998 Cast) x0 t0))))) (sn3_ind c (\lambda (t0: T).(\forall (x1: T).((eq T t0
999 (THead (Flat Appl) x x1)) \to (sn3 c (THead (Flat Appl) x (THead (Flat Cast)
1000 x0 x1)))))) (\lambda (t0: T).(\lambda (H6: ((\forall (t2: T).((((eq T t0 t2)
1001 \to (\forall (P: Prop).P))) \to ((pr3 c t0 t2) \to (sn3 c t2)))))).(\lambda
1002 (H7: ((\forall (t2: T).((((eq T t0 t2) \to (\forall (P: Prop).P))) \to ((pr3
1003 c t0 t2) \to (\forall (x1: T).((eq T t2 (THead (Flat Appl) x x1)) \to (sn3 c
1004 (THead (Flat Appl) x (THead (Flat Cast) x0 x1)))))))))).(\lambda (x1:
1005 T).(\lambda (H8: (eq T t0 (THead (Flat Appl) x x1))).(let H9 \def (eq_ind T
1006 t0 (\lambda (t2: T).(\forall (t3: T).((((eq T t2 t3) \to (\forall (P:
1007 Prop).P))) \to ((pr3 c t2 t3) \to (\forall (x2: T).((eq T t3 (THead (Flat
1008 Appl) x x2)) \to (sn3 c (THead (Flat Appl) x (THead (Flat Cast) x0
1009 x2))))))))) H7 (THead (Flat Appl) x x1) H8) in (let H10 \def (eq_ind T t0
1010 (\lambda (t2: T).(\forall (t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P)))
1011 \to ((pr3 c t2 t3) \to (sn3 c t3))))) H6 (THead (Flat Appl) x x1) H8) in (let
1012 H11 \def (eq_ind T t1 (\lambda (t2: T).(\forall (t3: T).((((eq T t2 t3) \to
1013 (\forall (P: Prop).P))) \to ((pr3 c t2 t3) \to (\forall (x2: T).(\forall (x3:
1014 T).((eq T t3 (THead (Flat Appl) x2 x3)) \to (\forall (t4: T).((sn3 c (THead
1015 (Flat Appl) x2 t4)) \to (sn3 c (THead (Flat Appl) x2 (THead (Flat Cast) x3
1016 t4)))))))))))) H2 (THead (Flat Appl) x x0) H3) in (let H12 \def (eq_ind T t1
1017 (\lambda (t2: T).(\forall (t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P)))
1018 \to ((pr3 c t2 t3) \to (sn3 c t3))))) H1 (THead (Flat Appl) x x0) H3) in
1019 (sn3_pr2_intro c (THead (Flat Appl) x (THead (Flat Cast) x0 x1)) (\lambda
1020 (t2: T).(\lambda (H13: (((eq T (THead (Flat Appl) x (THead (Flat Cast) x0
1021 x1)) t2) \to (\forall (P: Prop).P)))).(\lambda (H14: (pr2 c (THead (Flat
1022 Appl) x (THead (Flat Cast) x0 x1)) t2)).(let H15 \def (pr2_gen_appl c x
1023 (THead (Flat Cast) x0 x1) t2 H14) in (or3_ind (ex3_2 T T (\lambda (u2:
1024 T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
1025 T).(\lambda (_: T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c
1026 (THead (Flat Cast) x0 x1) t3)))) (ex4_4 T T T T (\lambda (y1: T).(\lambda
1027 (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Cast) x0 x1)
1028 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1029 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
1030 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
1031 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b:
1032 B).(\forall (u0: T).(pr2 (CHead c (Bind b) u0) z1 t3)))))))) (ex6_6 B T T T T
1033 T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1034 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
1035 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq
1036 T (THead (Flat Cast) x0 x1) (THead (Bind b) y1 z1)))))))) (\lambda (b:
1037 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
1038 (y2: T).(eq T t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2)
1039 z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1040 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_:
1041 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1042 (y2: T).(pr2 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
1043 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b)
1044 y2) z1 z2)))))))) (sn3 c t2) (\lambda (H16: (ex3_2 T T (\lambda (u2:
1045 T).(\lambda (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2:
1046 T).(\lambda (_: T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c
1047 (THead (Flat Cast) x0 x1) t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda
1048 (t3: T).(eq T t2 (THead (Flat Appl) u2 t3)))) (\lambda (u2: T).(\lambda (_:
1049 T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c (THead (Flat Cast)
1050 x0 x1) t3))) (sn3 c t2) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H17: (eq
1051 T t2 (THead (Flat Appl) x2 x3))).(\lambda (H18: (pr2 c x x2)).(\lambda (H19:
1052 (pr2 c (THead (Flat Cast) x0 x1) x3)).(let H20 \def (eq_ind T t2 (\lambda
1053 (t3: T).((eq T (THead (Flat Appl) x (THead (Flat Cast) x0 x1)) t3) \to
1054 (\forall (P: Prop).P))) H13 (THead (Flat Appl) x2 x3) H17) in (eq_ind_r T
1055 (THead (Flat Appl) x2 x3) (\lambda (t3: T).(sn3 c t3)) (let H21 \def
1056 (pr2_gen_cast c x0 x1 x3 H19) in (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda
1057 (t3: T).(eq T x3 (THead (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_:
1058 T).(pr2 c x0 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c x1 t3)))) (pr2 c
1059 x1 x3) (sn3 c (THead (Flat Appl) x2 x3)) (\lambda (H22: (ex3_2 T T (\lambda
1060 (u2: T).(\lambda (t3: T).(eq T x3 (THead (Flat Cast) u2 t3)))) (\lambda (u2:
1061 T).(\lambda (_: T).(pr2 c x0 u2))) (\lambda (_: T).(\lambda (t3: T).(pr2 c x1
1062 t3))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq T x3 (THead
1063 (Flat Cast) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2)))
1064 (\lambda (_: T).(\lambda (t3: T).(pr2 c x1 t3))) (sn3 c (THead (Flat Appl) x2
1065 x3)) (\lambda (x4: T).(\lambda (x5: T).(\lambda (H23: (eq T x3 (THead (Flat
1066 Cast) x4 x5))).(\lambda (H24: (pr2 c x0 x4)).(\lambda (H25: (pr2 c x1
1067 x5)).(let H26 \def (eq_ind T x3 (\lambda (t3: T).((eq T (THead (Flat Appl) x
1068 (THead (Flat Cast) x0 x1)) (THead (Flat Appl) x2 t3)) \to (\forall (P:
1069 Prop).P))) H20 (THead (Flat Cast) x4 x5) H23) in (eq_ind_r T (THead (Flat
1070 Cast) x4 x5) (\lambda (t3: T).(sn3 c (THead (Flat Appl) x2 t3))) (let H_x
1071 \def (term_dec (THead (Flat Appl) x x0) (THead (Flat Appl) x2 x4)) in (let
1072 H27 \def H_x in (or_ind (eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x2
1073 x4)) ((eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x2 x4)) \to (\forall
1074 (P: Prop).P)) (sn3 c (THead (Flat Appl) x2 (THead (Flat Cast) x4 x5)))
1075 (\lambda (H28: (eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x2
1076 x4))).(let H29 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
1077 \Rightarrow x | (TLRef _) \Rightarrow x | (THead _ t3 _) \Rightarrow t3]))
1078 (THead (Flat Appl) x x0) (THead (Flat Appl) x2 x4) H28) in ((let H30 \def
1079 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow x0 | (TLRef
1080 _) \Rightarrow x0 | (THead _ _ t3) \Rightarrow t3])) (THead (Flat Appl) x x0)
1081 (THead (Flat Appl) x2 x4) H28) in (\lambda (H31: (eq T x x2)).(let H32 \def
1082 (eq_ind_r T x4 (\lambda (t3: T).((eq T (THead (Flat Appl) x (THead (Flat
1083 Cast) x0 x1)) (THead (Flat Appl) x2 (THead (Flat Cast) t3 x5))) \to (\forall
1084 (P: Prop).P))) H26 x0 H30) in (let H33 \def (eq_ind_r T x4 (\lambda (t3:
1085 T).(pr2 c x0 t3)) H24 x0 H30) in (eq_ind T x0 (\lambda (t3: T).(sn3 c (THead
1086 (Flat Appl) x2 (THead (Flat Cast) t3 x5)))) (let H34 \def (eq_ind_r T x2
1087 (\lambda (t3: T).((eq T (THead (Flat Appl) x (THead (Flat Cast) x0 x1))
1088 (THead (Flat Appl) t3 (THead (Flat Cast) x0 x5))) \to (\forall (P: Prop).P)))
1089 H32 x H31) in (let H35 \def (eq_ind_r T x2 (\lambda (t3: T).(pr2 c x t3)) H18
1090 x H31) in (eq_ind T x (\lambda (t3: T).(sn3 c (THead (Flat Appl) t3 (THead
1091 (Flat Cast) x0 x5)))) (let H_x0 \def (term_dec (THead (Flat Appl) x x1)
1092 (THead (Flat Appl) x x5)) in (let H36 \def H_x0 in (or_ind (eq T (THead (Flat
1093 Appl) x x1) (THead (Flat Appl) x x5)) ((eq T (THead (Flat Appl) x x1) (THead
1094 (Flat Appl) x x5)) \to (\forall (P: Prop).P)) (sn3 c (THead (Flat Appl) x
1095 (THead (Flat Cast) x0 x5))) (\lambda (H37: (eq T (THead (Flat Appl) x x1)
1096 (THead (Flat Appl) x x5))).(let H38 \def (f_equal T T (\lambda (e: T).(match
1097 e with [(TSort _) \Rightarrow x1 | (TLRef _) \Rightarrow x1 | (THead _ _ t3)
1098 \Rightarrow t3])) (THead (Flat Appl) x x1) (THead (Flat Appl) x x5) H37) in
1099 (let H39 \def (eq_ind_r T x5 (\lambda (t3: T).((eq T (THead (Flat Appl) x
1100 (THead (Flat Cast) x0 x1)) (THead (Flat Appl) x (THead (Flat Cast) x0 t3)))
1101 \to (\forall (P: Prop).P))) H34 x1 H38) in (let H40 \def (eq_ind_r T x5
1102 (\lambda (t3: T).(pr2 c x1 t3)) H25 x1 H38) in (eq_ind T x1 (\lambda (t3:
1103 T).(sn3 c (THead (Flat Appl) x (THead (Flat Cast) x0 t3)))) (H39 (refl_equal
1104 T (THead (Flat Appl) x (THead (Flat Cast) x0 x1))) (sn3 c (THead (Flat Appl)
1105 x (THead (Flat Cast) x0 x1)))) x5 H38))))) (\lambda (H37: (((eq T (THead
1106 (Flat Appl) x x1) (THead (Flat Appl) x x5)) \to (\forall (P: Prop).P)))).(H9
1107 (THead (Flat Appl) x x5) H37 (pr3_pr2 c (THead (Flat Appl) x x1) (THead (Flat
1108 Appl) x x5) (pr2_thin_dx c x1 x5 H25 x Appl)) x5 (refl_equal T (THead (Flat
1109 Appl) x x5)))) H36))) x2 H31))) x4 H30))))) H29))) (\lambda (H28: (((eq T
1110 (THead (Flat Appl) x x0) (THead (Flat Appl) x2 x4)) \to (\forall (P:
1111 Prop).P)))).(let H_x0 \def (term_dec (THead (Flat Appl) x x1) (THead (Flat
1112 Appl) x2 x5)) in (let H29 \def H_x0 in (or_ind (eq T (THead (Flat Appl) x x1)
1113 (THead (Flat Appl) x2 x5)) ((eq T (THead (Flat Appl) x x1) (THead (Flat Appl)
1114 x2 x5)) \to (\forall (P: Prop).P)) (sn3 c (THead (Flat Appl) x2 (THead (Flat
1115 Cast) x4 x5))) (\lambda (H30: (eq T (THead (Flat Appl) x x1) (THead (Flat
1116 Appl) x2 x5))).(let H31 \def (f_equal T T (\lambda (e: T).(match e with
1117 [(TSort _) \Rightarrow x | (TLRef _) \Rightarrow x | (THead _ t3 _)
1118 \Rightarrow t3])) (THead (Flat Appl) x x1) (THead (Flat Appl) x2 x5) H30) in
1119 ((let H32 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
1120 \Rightarrow x1 | (TLRef _) \Rightarrow x1 | (THead _ _ t3) \Rightarrow t3]))
1121 (THead (Flat Appl) x x1) (THead (Flat Appl) x2 x5) H30) in (\lambda (H33: (eq
1122 T x x2)).(let H34 \def (eq_ind_r T x5 (\lambda (t3: T).(pr2 c x1 t3)) H25 x1
1123 H32) in (eq_ind T x1 (\lambda (t3: T).(sn3 c (THead (Flat Appl) x2 (THead
1124 (Flat Cast) x4 t3)))) (let H35 \def (eq_ind_r T x2 (\lambda (t3: T).((eq T
1125 (THead (Flat Appl) x x0) (THead (Flat Appl) t3 x4)) \to (\forall (P:
1126 Prop).P))) H28 x H33) in (let H36 \def (eq_ind_r T x2 (\lambda (t3: T).(pr2 c
1127 x t3)) H18 x H33) in (eq_ind T x (\lambda (t3: T).(sn3 c (THead (Flat Appl)
1128 t3 (THead (Flat Cast) x4 x1)))) (H11 (THead (Flat Appl) x x4) H35 (pr3_pr2 c
1129 (THead (Flat Appl) x x0) (THead (Flat Appl) x x4) (pr2_thin_dx c x0 x4 H24 x
1130 Appl)) x x4 (refl_equal T (THead (Flat Appl) x x4)) x1 (sn3_sing c (THead
1131 (Flat Appl) x x1) H10)) x2 H33))) x5 H32)))) H31))) (\lambda (H30: (((eq T
1132 (THead (Flat Appl) x x1) (THead (Flat Appl) x2 x5)) \to (\forall (P:
1133 Prop).P)))).(H11 (THead (Flat Appl) x2 x4) H28 (pr3_flat c x x2 (pr3_pr2 c x
1134 x2 H18) x0 x4 (pr3_pr2 c x0 x4 H24) Appl) x2 x4 (refl_equal T (THead (Flat
1135 Appl) x2 x4)) x5 (H10 (THead (Flat Appl) x2 x5) H30 (pr3_flat c x x2 (pr3_pr2
1136 c x x2 H18) x1 x5 (pr3_pr2 c x1 x5 H25) Appl)))) H29)))) H27))) x3 H23)))))))
1137 H22)) (\lambda (H22: (pr2 c x1 x3)).(let H_x \def (term_dec (THead (Flat
1138 Appl) x x1) (THead (Flat Appl) x2 x3)) in (let H23 \def H_x in (or_ind (eq T
1139 (THead (Flat Appl) x x1) (THead (Flat Appl) x2 x3)) ((eq T (THead (Flat Appl)
1140 x x1) (THead (Flat Appl) x2 x3)) \to (\forall (P: Prop).P)) (sn3 c (THead
1141 (Flat Appl) x2 x3)) (\lambda (H24: (eq T (THead (Flat Appl) x x1) (THead
1142 (Flat Appl) x2 x3))).(let H25 \def (f_equal T T (\lambda (e: T).(match e with
1143 [(TSort _) \Rightarrow x | (TLRef _) \Rightarrow x | (THead _ t3 _)
1144 \Rightarrow t3])) (THead (Flat Appl) x x1) (THead (Flat Appl) x2 x3) H24) in
1145 ((let H26 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
1146 \Rightarrow x1 | (TLRef _) \Rightarrow x1 | (THead _ _ t3) \Rightarrow t3]))
1147 (THead (Flat Appl) x x1) (THead (Flat Appl) x2 x3) H24) in (\lambda (H27: (eq
1148 T x x2)).(let H28 \def (eq_ind_r T x3 (\lambda (t3: T).(pr2 c x1 t3)) H22 x1
1149 H26) in (let H29 \def (eq_ind_r T x3 (\lambda (t3: T).((eq T (THead (Flat
1150 Appl) x (THead (Flat Cast) x0 x1)) (THead (Flat Appl) x2 t3)) \to (\forall
1151 (P: Prop).P))) H20 x1 H26) in (eq_ind T x1 (\lambda (t3: T).(sn3 c (THead
1152 (Flat Appl) x2 t3))) (let H30 \def (eq_ind_r T x2 (\lambda (t3: T).((eq T
1153 (THead (Flat Appl) x (THead (Flat Cast) x0 x1)) (THead (Flat Appl) t3 x1))
1154 \to (\forall (P: Prop).P))) H29 x H27) in (let H31 \def (eq_ind_r T x2
1155 (\lambda (t3: T).(pr2 c x t3)) H18 x H27) in (eq_ind T x (\lambda (t3:
1156 T).(sn3 c (THead (Flat Appl) t3 x1))) (sn3_sing c (THead (Flat Appl) x x1)
1157 H10) x2 H27))) x3 H26))))) H25))) (\lambda (H24: (((eq T (THead (Flat Appl) x
1158 x1) (THead (Flat Appl) x2 x3)) \to (\forall (P: Prop).P)))).(H10 (THead (Flat
1159 Appl) x2 x3) H24 (pr3_flat c x x2 (pr3_pr2 c x x2 H18) x1 x3 (pr3_pr2 c x1 x3
1160 H22) Appl))) H23)))) H21)) t2 H17))))))) H16)) (\lambda (H16: (ex4_4 T T T T
1161 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
1162 (THead (Flat Cast) x0 x1) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
1163 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
1164 Abbr) u2 t3)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1165 (_: T).(pr2 c x u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1166 T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b)
1167 u0) z1 t3))))))))).(ex4_4_ind T T T T (\lambda (y1: T).(\lambda (z1:
1168 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Cast) x0 x1) (THead
1169 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1170 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))))) (\lambda (_:
1171 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
1172 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t3: T).(\forall (b:
1173 B).(\forall (u0: T).(pr2 (CHead c (Bind b) u0) z1 t3))))))) (sn3 c t2)
1174 (\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda
1175 (H17: (eq T (THead (Flat Cast) x0 x1) (THead (Bind Abst) x2 x3))).(\lambda
1176 (H18: (eq T t2 (THead (Bind Abbr) x4 x5))).(\lambda (_: (pr2 c x
1177 x4)).(\lambda (_: ((\forall (b: B).(\forall (u0: T).(pr2 (CHead c (Bind b)
1178 u0) x3 x5))))).(let H21 \def (eq_ind T t2 (\lambda (t3: T).((eq T (THead
1179 (Flat Appl) x (THead (Flat Cast) x0 x1)) t3) \to (\forall (P: Prop).P))) H13
1180 (THead (Bind Abbr) x4 x5) H18) in (eq_ind_r T (THead (Bind Abbr) x4 x5)
1181 (\lambda (t3: T).(sn3 c t3)) (let H22 \def (eq_ind T (THead (Flat Cast) x0
1182 x1) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
1183 \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
1184 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abst) x2
1185 x3) H17) in (False_ind (sn3 c (THead (Bind Abbr) x4 x5)) H22)) t2
1186 H18)))))))))) H16)) (\lambda (H16: (ex6_6 B T T T T T (\lambda (b:
1187 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1188 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
1189 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat
1190 Cast) x0 x1) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
1191 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
1192 t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
1193 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1194 T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1:
1195 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
1196 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
1197 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1
1198 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda
1199 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b
1200 Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
1201 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Cast) x0 x1) (THead
1202 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
1203 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
1204 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
1205 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1206 (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1207 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
1208 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1209 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))) (sn3 c t2)
1210 (\lambda (x2: B).(\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda
1211 (x6: T).(\lambda (x7: T).(\lambda (_: (not (eq B x2 Abst))).(\lambda (H18:
1212 (eq T (THead (Flat Cast) x0 x1) (THead (Bind x2) x3 x4))).(\lambda (H19: (eq
1213 T t2 (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) O x6) x5)))).(\lambda
1214 (_: (pr2 c x x6)).(\lambda (_: (pr2 c x3 x7)).(\lambda (_: (pr2 (CHead c
1215 (Bind x2) x7) x4 x5)).(let H23 \def (eq_ind T t2 (\lambda (t3: T).((eq T
1216 (THead (Flat Appl) x (THead (Flat Cast) x0 x1)) t3) \to (\forall (P:
1217 Prop).P))) H13 (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) O x6) x5))
1218 H19) in (eq_ind_r T (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) O x6)
1219 x5)) (\lambda (t3: T).(sn3 c t3)) (let H24 \def (eq_ind T (THead (Flat Cast)
1220 x0 x1) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef
1221 _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
1222 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind x2) x3 x4)
1223 H18) in (False_ind (sn3 c (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O)
1224 O x6) x5))) H24)) t2 H19)))))))))))))) H16)) H15))))))))))))))) y0 H5))))
1225 H4))))))))) y H0))))) H)))).
1227 theorem sn3_appl_bind:
1228 \forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (u:
1229 T).((sn3 c u) \to (\forall (t: T).(\forall (v: T).((sn3 (CHead c (Bind b) u)
1230 (THead (Flat Appl) (lift (S O) O v) t)) \to (sn3 c (THead (Flat Appl) v
1231 (THead (Bind b) u t))))))))))
1233 \lambda (b: B).(\lambda (H: (not (eq B b Abst))).(\lambda (c: C).(\lambda
1234 (u: T).(\lambda (H0: (sn3 c u)).(sn3_ind c (\lambda (t: T).(\forall (t0:
1235 T).(\forall (v: T).((sn3 (CHead c (Bind b) t) (THead (Flat Appl) (lift (S O)
1236 O v) t0)) \to (sn3 c (THead (Flat Appl) v (THead (Bind b) t t0)))))))
1237 (\lambda (t1: T).(\lambda (H1: ((\forall (t2: T).((((eq T t1 t2) \to (\forall
1238 (P: Prop).P))) \to ((pr3 c t1 t2) \to (sn3 c t2)))))).(\lambda (H2: ((\forall
1239 (t2: T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 c t1 t2) \to
1240 (\forall (t: T).(\forall (v: T).((sn3 (CHead c (Bind b) t2) (THead (Flat
1241 Appl) (lift (S O) O v) t)) \to (sn3 c (THead (Flat Appl) v (THead (Bind b) t2
1242 t))))))))))).(\lambda (t: T).(\lambda (v: T).(\lambda (H3: (sn3 (CHead c
1243 (Bind b) t1) (THead (Flat Appl) (lift (S O) O v) t))).(insert_eq T (THead
1244 (Flat Appl) (lift (S O) O v) t) (\lambda (t0: T).(sn3 (CHead c (Bind b) t1)
1245 t0)) (\lambda (_: T).(sn3 c (THead (Flat Appl) v (THead (Bind b) t1 t))))
1246 (\lambda (y: T).(\lambda (H4: (sn3 (CHead c (Bind b) t1) y)).(unintro T t
1247 (\lambda (t0: T).((eq T y (THead (Flat Appl) (lift (S O) O v) t0)) \to (sn3 c
1248 (THead (Flat Appl) v (THead (Bind b) t1 t0))))) (unintro T v (\lambda (t0:
1249 T).(\forall (x: T).((eq T y (THead (Flat Appl) (lift (S O) O t0) x)) \to (sn3
1250 c (THead (Flat Appl) t0 (THead (Bind b) t1 x)))))) (sn3_ind (CHead c (Bind b)
1251 t1) (\lambda (t0: T).(\forall (x: T).(\forall (x0: T).((eq T t0 (THead (Flat
1252 Appl) (lift (S O) O x) x0)) \to (sn3 c (THead (Flat Appl) x (THead (Bind b)
1253 t1 x0))))))) (\lambda (t2: T).(\lambda (H5: ((\forall (t3: T).((((eq T t2 t3)
1254 \to (\forall (P: Prop).P))) \to ((pr3 (CHead c (Bind b) t1) t2 t3) \to (sn3
1255 (CHead c (Bind b) t1) t3)))))).(\lambda (H6: ((\forall (t3: T).((((eq T t2
1256 t3) \to (\forall (P: Prop).P))) \to ((pr3 (CHead c (Bind b) t1) t2 t3) \to
1257 (\forall (x: T).(\forall (x0: T).((eq T t3 (THead (Flat Appl) (lift (S O) O
1258 x) x0)) \to (sn3 c (THead (Flat Appl) x (THead (Bind b) t1
1259 x0))))))))))).(\lambda (x: T).(\lambda (x0: T).(\lambda (H7: (eq T t2 (THead
1260 (Flat Appl) (lift (S O) O x) x0))).(let H8 \def (eq_ind T t2 (\lambda (t0:
1261 T).(\forall (t3: T).((((eq T t0 t3) \to (\forall (P: Prop).P))) \to ((pr3
1262 (CHead c (Bind b) t1) t0 t3) \to (\forall (x1: T).(\forall (x2: T).((eq T t3
1263 (THead (Flat Appl) (lift (S O) O x1) x2)) \to (sn3 c (THead (Flat Appl) x1
1264 (THead (Bind b) t1 x2)))))))))) H6 (THead (Flat Appl) (lift (S O) O x) x0)
1265 H7) in (let H9 \def (eq_ind T t2 (\lambda (t0: T).(\forall (t3: T).((((eq T
1266 t0 t3) \to (\forall (P: Prop).P))) \to ((pr3 (CHead c (Bind b) t1) t0 t3) \to
1267 (sn3 (CHead c (Bind b) t1) t3))))) H5 (THead (Flat Appl) (lift (S O) O x) x0)
1268 H7) in (sn3_pr2_intro c (THead (Flat Appl) x (THead (Bind b) t1 x0)) (\lambda
1269 (t3: T).(\lambda (H10: (((eq T (THead (Flat Appl) x (THead (Bind b) t1 x0))
1270 t3) \to (\forall (P: Prop).P)))).(\lambda (H11: (pr2 c (THead (Flat Appl) x
1271 (THead (Bind b) t1 x0)) t3)).(let H12 \def (pr2_gen_appl c x (THead (Bind b)
1272 t1 x0) t3 H11) in (or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T
1273 t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x
1274 u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c (THead (Bind b) t1 x0) t4))))
1275 (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
1276 T).(eq T (THead (Bind b) t1 x0) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
1277 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind
1278 Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1279 (_: T).(pr2 c x u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1280 T).(\lambda (t4: T).(\forall (b0: B).(\forall (u0: T).(pr2 (CHead c (Bind b0)
1281 u0) z1 t4)))))))) (ex6_6 B T T T T T (\lambda (b0: B).(\lambda (_:
1282 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
1283 b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda
1284 (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind b) t1 x0) (THead
1285 (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
1286 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t3 (THead (Bind
1287 b0) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
1288 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1289 (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1290 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
1291 (\lambda (b0: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1292 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b0) y2) z1 z2)))))))) (sn3 c t3)
1293 (\lambda (H13: (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead
1294 (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
1295 (\lambda (_: T).(\lambda (t4: T).(pr2 c (THead (Bind b) t1 x0)
1296 t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead
1297 (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
1298 (\lambda (_: T).(\lambda (t4: T).(pr2 c (THead (Bind b) t1 x0) t4))) (sn3 c
1299 t3) (\lambda (x1: T).(\lambda (x2: T).(\lambda (H14: (eq T t3 (THead (Flat
1300 Appl) x1 x2))).(\lambda (H15: (pr2 c x x1)).(\lambda (H16: (pr2 c (THead
1301 (Bind b) t1 x0) x2)).(let H17 \def (eq_ind T t3 (\lambda (t0: T).((eq T
1302 (THead (Flat Appl) x (THead (Bind b) t1 x0)) t0) \to (\forall (P: Prop).P)))
1303 H10 (THead (Flat Appl) x1 x2) H14) in (eq_ind_r T (THead (Flat Appl) x1 x2)
1304 (\lambda (t0: T).(sn3 c t0)) (let H_x \def (pr3_gen_bind b H c t1 x0 x2) in
1305 (let H18 \def (H_x (pr3_pr2 c (THead (Bind b) t1 x0) x2 H16)) in (or_ind
1306 (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T x2 (THead (Bind b) u2
1307 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c t1 u2))) (\lambda (_:
1308 T).(\lambda (t4: T).(pr3 (CHead c (Bind b) t1) x0 t4)))) (pr3 (CHead c (Bind
1309 b) t1) x0 (lift (S O) O x2)) (sn3 c (THead (Flat Appl) x1 x2)) (\lambda (H19:
1310 (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T x2 (THead (Bind b) u2
1311 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c t1 u2))) (\lambda (_:
1312 T).(\lambda (t4: T).(pr3 (CHead c (Bind b) t1) x0 t4))))).(ex3_2_ind T T
1313 (\lambda (u2: T).(\lambda (t4: T).(eq T x2 (THead (Bind b) u2 t4)))) (\lambda
1314 (u2: T).(\lambda (_: T).(pr3 c t1 u2))) (\lambda (_: T).(\lambda (t4: T).(pr3
1315 (CHead c (Bind b) t1) x0 t4))) (sn3 c (THead (Flat Appl) x1 x2)) (\lambda
1316 (x3: T).(\lambda (x4: T).(\lambda (H20: (eq T x2 (THead (Bind b) x3
1317 x4))).(\lambda (H21: (pr3 c t1 x3)).(\lambda (H22: (pr3 (CHead c (Bind b) t1)
1318 x0 x4)).(let H23 \def (eq_ind T x2 (\lambda (t0: T).((eq T (THead (Flat Appl)
1319 x (THead (Bind b) t1 x0)) (THead (Flat Appl) x1 t0)) \to (\forall (P:
1320 Prop).P))) H17 (THead (Bind b) x3 x4) H20) in (eq_ind_r T (THead (Bind b) x3
1321 x4) (\lambda (t0: T).(sn3 c (THead (Flat Appl) x1 t0))) (let H_x0 \def
1322 (term_dec t1 x3) in (let H24 \def H_x0 in (or_ind (eq T t1 x3) ((eq T t1 x3)
1323 \to (\forall (P: Prop).P)) (sn3 c (THead (Flat Appl) x1 (THead (Bind b) x3
1324 x4))) (\lambda (H25: (eq T t1 x3)).(let H26 \def (eq_ind_r T x3 (\lambda (t0:
1325 T).((eq T (THead (Flat Appl) x (THead (Bind b) t1 x0)) (THead (Flat Appl) x1
1326 (THead (Bind b) t0 x4))) \to (\forall (P: Prop).P))) H23 t1 H25) in (let H27
1327 \def (eq_ind_r T x3 (\lambda (t0: T).(pr3 c t1 t0)) H21 t1 H25) in (eq_ind T
1328 t1 (\lambda (t0: T).(sn3 c (THead (Flat Appl) x1 (THead (Bind b) t0 x4))))
1329 (let H_x1 \def (term_dec x0 x4) in (let H28 \def H_x1 in (or_ind (eq T x0 x4)
1330 ((eq T x0 x4) \to (\forall (P: Prop).P)) (sn3 c (THead (Flat Appl) x1 (THead
1331 (Bind b) t1 x4))) (\lambda (H29: (eq T x0 x4)).(let H30 \def (eq_ind_r T x4
1332 (\lambda (t0: T).((eq T (THead (Flat Appl) x (THead (Bind b) t1 x0)) (THead
1333 (Flat Appl) x1 (THead (Bind b) t1 t0))) \to (\forall (P: Prop).P))) H26 x0
1334 H29) in (let H31 \def (eq_ind_r T x4 (\lambda (t0: T).(pr3 (CHead c (Bind b)
1335 t1) x0 t0)) H22 x0 H29) in (eq_ind T x0 (\lambda (t0: T).(sn3 c (THead (Flat
1336 Appl) x1 (THead (Bind b) t1 t0)))) (let H_x2 \def (term_dec x x1) in (let H32
1337 \def H_x2 in (or_ind (eq T x x1) ((eq T x x1) \to (\forall (P: Prop).P)) (sn3
1338 c (THead (Flat Appl) x1 (THead (Bind b) t1 x0))) (\lambda (H33: (eq T x
1339 x1)).(let H34 \def (eq_ind_r T x1 (\lambda (t0: T).((eq T (THead (Flat Appl)
1340 x (THead (Bind b) t1 x0)) (THead (Flat Appl) t0 (THead (Bind b) t1 x0))) \to
1341 (\forall (P: Prop).P))) H30 x H33) in (let H35 \def (eq_ind_r T x1 (\lambda
1342 (t0: T).(pr2 c x t0)) H15 x H33) in (eq_ind T x (\lambda (t0: T).(sn3 c
1343 (THead (Flat Appl) t0 (THead (Bind b) t1 x0)))) (H34 (refl_equal T (THead
1344 (Flat Appl) x (THead (Bind b) t1 x0))) (sn3 c (THead (Flat Appl) x (THead
1345 (Bind b) t1 x0)))) x1 H33)))) (\lambda (H33: (((eq T x x1) \to (\forall (P:
1346 Prop).P)))).(H8 (THead (Flat Appl) (lift (S O) O x1) x0) (\lambda (H34: (eq T
1347 (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat Appl) (lift (S O) O x1)
1348 x0))).(\lambda (P: Prop).(let H35 \def (f_equal T T (\lambda (e: T).(match e
1349 with [(TSort _) \Rightarrow (lref_map (\lambda (x5: nat).(plus x5 (S O))) O
1350 x) | (TLRef _) \Rightarrow (lref_map (\lambda (x5: nat).(plus x5 (S O))) O x)
1351 | (THead _ t0 _) \Rightarrow t0])) (THead (Flat Appl) (lift (S O) O x) x0)
1352 (THead (Flat Appl) (lift (S O) O x1) x0) H34) in (let H36 \def (eq_ind_r T x1
1353 (\lambda (t0: T).((eq T x t0) \to (\forall (P0: Prop).P0))) H33 x (lift_inj x
1354 x1 (S O) O H35)) in (let H37 \def (eq_ind_r T x1 (\lambda (t0: T).(pr2 c x
1355 t0)) H15 x (lift_inj x x1 (S O) O H35)) in (H36 (refl_equal T x) P))))))
1356 (pr3_flat (CHead c (Bind b) t1) (lift (S O) O x) (lift (S O) O x1) (pr3_lift
1357 (CHead c (Bind b) t1) c (S O) O (drop_drop (Bind b) O c c (drop_refl c) t1) x
1358 x1 (pr3_pr2 c x x1 H15)) x0 x0 (pr3_refl (CHead c (Bind b) t1) x0) Appl) x1
1359 x0 (refl_equal T (THead (Flat Appl) (lift (S O) O x1) x0)))) H32))) x4
1360 H29)))) (\lambda (H29: (((eq T x0 x4) \to (\forall (P: Prop).P)))).(H8 (THead
1361 (Flat Appl) (lift (S O) O x1) x4) (\lambda (H30: (eq T (THead (Flat Appl)
1362 (lift (S O) O x) x0) (THead (Flat Appl) (lift (S O) O x1) x4))).(\lambda (P:
1363 Prop).(let H31 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
1364 \Rightarrow (lref_map (\lambda (x5: nat).(plus x5 (S O))) O x) | (TLRef _)
1365 \Rightarrow (lref_map (\lambda (x5: nat).(plus x5 (S O))) O x) | (THead _ t0
1366 _) \Rightarrow t0])) (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat
1367 Appl) (lift (S O) O x1) x4) H30) in ((let H32 \def (f_equal T T (\lambda (e:
1368 T).(match e with [(TSort _) \Rightarrow x0 | (TLRef _) \Rightarrow x0 |
1369 (THead _ _ t0) \Rightarrow t0])) (THead (Flat Appl) (lift (S O) O x) x0)
1370 (THead (Flat Appl) (lift (S O) O x1) x4) H30) in (\lambda (H33: (eq T (lift
1371 (S O) O x) (lift (S O) O x1))).(let H34 \def (eq_ind_r T x4 (\lambda (t0:
1372 T).((eq T x0 t0) \to (\forall (P0: Prop).P0))) H29 x0 H32) in (let H35 \def
1373 (eq_ind_r T x4 (\lambda (t0: T).((eq T (THead (Flat Appl) x (THead (Bind b)
1374 t1 x0)) (THead (Flat Appl) x1 (THead (Bind b) t1 t0))) \to (\forall (P0:
1375 Prop).P0))) H26 x0 H32) in (let H36 \def (eq_ind_r T x4 (\lambda (t0: T).(pr3
1376 (CHead c (Bind b) t1) x0 t0)) H22 x0 H32) in (let H37 \def (eq_ind_r T x1
1377 (\lambda (t0: T).((eq T (THead (Flat Appl) x (THead (Bind b) t1 x0)) (THead
1378 (Flat Appl) t0 (THead (Bind b) t1 x0))) \to (\forall (P0: Prop).P0))) H35 x
1379 (lift_inj x x1 (S O) O H33)) in (let H38 \def (eq_ind_r T x1 (\lambda (t0:
1380 T).(pr2 c x t0)) H15 x (lift_inj x x1 (S O) O H33)) in (H34 (refl_equal T x0)
1381 P)))))))) H31)))) (pr3_flat (CHead c (Bind b) t1) (lift (S O) O x) (lift (S
1382 O) O x1) (pr3_lift (CHead c (Bind b) t1) c (S O) O (drop_drop (Bind b) O c c
1383 (drop_refl c) t1) x x1 (pr3_pr2 c x x1 H15)) x0 x4 H22 Appl) x1 x4
1384 (refl_equal T (THead (Flat Appl) (lift (S O) O x1) x4)))) H28))) x3 H25))))
1385 (\lambda (H25: (((eq T t1 x3) \to (\forall (P: Prop).P)))).(H2 x3 H25 H21 x4
1386 x1 (sn3_cpr3_trans c t1 x3 H21 (Bind b) (THead (Flat Appl) (lift (S O) O x1)
1387 x4) (let H_x1 \def (term_dec x0 x4) in (let H26 \def H_x1 in (or_ind (eq T x0
1388 x4) ((eq T x0 x4) \to (\forall (P: Prop).P)) (sn3 (CHead c (Bind b) t1)
1389 (THead (Flat Appl) (lift (S O) O x1) x4)) (\lambda (H27: (eq T x0 x4)).(let
1390 H28 \def (eq_ind_r T x4 (\lambda (t0: T).(pr3 (CHead c (Bind b) t1) x0 t0))
1391 H22 x0 H27) in (eq_ind T x0 (\lambda (t0: T).(sn3 (CHead c (Bind b) t1)
1392 (THead (Flat Appl) (lift (S O) O x1) t0))) (let H_x2 \def (term_dec x x1) in
1393 (let H29 \def H_x2 in (or_ind (eq T x x1) ((eq T x x1) \to (\forall (P:
1394 Prop).P)) (sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1)
1395 x0)) (\lambda (H30: (eq T x x1)).(let H31 \def (eq_ind_r T x1 (\lambda (t0:
1396 T).(pr2 c x t0)) H15 x H30) in (eq_ind T x (\lambda (t0: T).(sn3 (CHead c
1397 (Bind b) t1) (THead (Flat Appl) (lift (S O) O t0) x0))) (sn3_sing (CHead c
1398 (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x0) H9) x1 H30))) (\lambda
1399 (H30: (((eq T x x1) \to (\forall (P: Prop).P)))).(H9 (THead (Flat Appl) (lift
1400 (S O) O x1) x0) (\lambda (H31: (eq T (THead (Flat Appl) (lift (S O) O x) x0)
1401 (THead (Flat Appl) (lift (S O) O x1) x0))).(\lambda (P: Prop).(let H32 \def
1402 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow (lref_map
1403 (\lambda (x5: nat).(plus x5 (S O))) O x) | (TLRef _) \Rightarrow (lref_map
1404 (\lambda (x5: nat).(plus x5 (S O))) O x) | (THead _ t0 _) \Rightarrow t0]))
1405 (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat Appl) (lift (S O) O x1)
1406 x0) H31) in (let H33 \def (eq_ind_r T x1 (\lambda (t0: T).((eq T x t0) \to
1407 (\forall (P0: Prop).P0))) H30 x (lift_inj x x1 (S O) O H32)) in (let H34 \def
1408 (eq_ind_r T x1 (\lambda (t0: T).(pr2 c x t0)) H15 x (lift_inj x x1 (S O) O
1409 H32)) in (H33 (refl_equal T x) P)))))) (pr3_flat (CHead c (Bind b) t1) (lift
1410 (S O) O x) (lift (S O) O x1) (pr3_lift (CHead c (Bind b) t1) c (S O) O
1411 (drop_drop (Bind b) O c c (drop_refl c) t1) x x1 (pr3_pr2 c x x1 H15)) x0 x0
1412 (pr3_refl (CHead c (Bind b) t1) x0) Appl))) H29))) x4 H27))) (\lambda (H27:
1413 (((eq T x0 x4) \to (\forall (P: Prop).P)))).(H9 (THead (Flat Appl) (lift (S
1414 O) O x1) x4) (\lambda (H28: (eq T (THead (Flat Appl) (lift (S O) O x) x0)
1415 (THead (Flat Appl) (lift (S O) O x1) x4))).(\lambda (P: Prop).(let H29 \def
1416 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow (lref_map
1417 (\lambda (x5: nat).(plus x5 (S O))) O x) | (TLRef _) \Rightarrow (lref_map
1418 (\lambda (x5: nat).(plus x5 (S O))) O x) | (THead _ t0 _) \Rightarrow t0]))
1419 (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat Appl) (lift (S O) O x1)
1420 x4) H28) in ((let H30 \def (f_equal T T (\lambda (e: T).(match e with [(TSort
1421 _) \Rightarrow x0 | (TLRef _) \Rightarrow x0 | (THead _ _ t0) \Rightarrow
1422 t0])) (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat Appl) (lift (S O)
1423 O x1) x4) H28) in (\lambda (H31: (eq T (lift (S O) O x) (lift (S O) O
1424 x1))).(let H32 \def (eq_ind_r T x4 (\lambda (t0: T).((eq T x0 t0) \to
1425 (\forall (P0: Prop).P0))) H27 x0 H30) in (let H33 \def (eq_ind_r T x4
1426 (\lambda (t0: T).(pr3 (CHead c (Bind b) t1) x0 t0)) H22 x0 H30) in (let H34
1427 \def (eq_ind_r T x1 (\lambda (t0: T).(pr2 c x t0)) H15 x (lift_inj x x1 (S O)
1428 O H31)) in (H32 (refl_equal T x0) P)))))) H29)))) (pr3_flat (CHead c (Bind b)
1429 t1) (lift (S O) O x) (lift (S O) O x1) (pr3_lift (CHead c (Bind b) t1) c (S
1430 O) O (drop_drop (Bind b) O c c (drop_refl c) t1) x x1 (pr3_pr2 c x x1 H15))
1431 x0 x4 H22 Appl))) H26)))))) H24))) x2 H20))))))) H19)) (\lambda (H19: (pr3
1432 (CHead c (Bind b) t1) x0 (lift (S O) O x2))).(sn3_gen_lift (CHead c (Bind b)
1433 t1) (THead (Flat Appl) x1 x2) (S O) O (eq_ind_r T (THead (Flat Appl) (lift (S
1434 O) O x1) (lift (S O) (s (Flat Appl) O) x2)) (\lambda (t0: T).(sn3 (CHead c
1435 (Bind b) t1) t0)) (sn3_pr3_trans (CHead c (Bind b) t1) (THead (Flat Appl)
1436 (lift (S O) O x1) x0) (let H_x0 \def (term_dec x x1) in (let H20 \def H_x0 in
1437 (or_ind (eq T x x1) ((eq T x x1) \to (\forall (P: Prop).P)) (sn3 (CHead c
1438 (Bind b) t1) (THead (Flat Appl) (lift (S O) O x1) x0)) (\lambda (H21: (eq T x
1439 x1)).(let H22 \def (eq_ind_r T x1 (\lambda (t0: T).(pr2 c x t0)) H15 x H21)
1440 in (eq_ind T x (\lambda (t0: T).(sn3 (CHead c (Bind b) t1) (THead (Flat Appl)
1441 (lift (S O) O t0) x0))) (sn3_sing (CHead c (Bind b) t1) (THead (Flat Appl)
1442 (lift (S O) O x) x0) H9) x1 H21))) (\lambda (H21: (((eq T x x1) \to (\forall
1443 (P: Prop).P)))).(H9 (THead (Flat Appl) (lift (S O) O x1) x0) (\lambda (H22:
1444 (eq T (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat Appl) (lift (S O)
1445 O x1) x0))).(\lambda (P: Prop).(let H23 \def (f_equal T T (\lambda (e:
1446 T).(match e with [(TSort _) \Rightarrow (lref_map (\lambda (x3: nat).(plus x3
1447 (S O))) O x) | (TLRef _) \Rightarrow (lref_map (\lambda (x3: nat).(plus x3 (S
1448 O))) O x) | (THead _ t0 _) \Rightarrow t0])) (THead (Flat Appl) (lift (S O) O
1449 x) x0) (THead (Flat Appl) (lift (S O) O x1) x0) H22) in (let H24 \def
1450 (eq_ind_r T x1 (\lambda (t0: T).((eq T x t0) \to (\forall (P0: Prop).P0)))
1451 H21 x (lift_inj x x1 (S O) O H23)) in (let H25 \def (eq_ind_r T x1 (\lambda
1452 (t0: T).(pr2 c x t0)) H15 x (lift_inj x x1 (S O) O H23)) in (H24 (refl_equal
1453 T x) P)))))) (pr3_flat (CHead c (Bind b) t1) (lift (S O) O x) (lift (S O) O
1454 x1) (pr3_lift (CHead c (Bind b) t1) c (S O) O (drop_drop (Bind b) O c c
1455 (drop_refl c) t1) x x1 (pr3_pr2 c x x1 H15)) x0 x0 (pr3_refl (CHead c (Bind
1456 b) t1) x0) Appl))) H20))) (THead (Flat Appl) (lift (S O) O x1) (lift (S O) O
1457 x2)) (pr3_thin_dx (CHead c (Bind b) t1) x0 (lift (S O) O x2) H19 (lift (S O)
1458 O x1) Appl)) (lift (S O) O (THead (Flat Appl) x1 x2)) (lift_head (Flat Appl)
1459 x1 x2 (S O) O)) c (drop_drop (Bind b) O c c (drop_refl c) t1))) H18))) t3
1460 H14))))))) H13)) (\lambda (H13: (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1:
1461 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind b) t1 x0) (THead (Bind
1462 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1463 (t4: T).(eq T t3 (THead (Bind Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_:
1464 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda (_: T).(\lambda
1465 (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b0: B).(\forall (u0:
1466 T).(pr2 (CHead c (Bind b0) u0) z1 t4))))))))).(ex4_4_ind T T T T (\lambda
1467 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind
1468 b) t1 x0) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_:
1469 T).(\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind Abbr) u2 t4))))))
1470 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x
1471 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4:
1472 T).(\forall (b0: B).(\forall (u0: T).(pr2 (CHead c (Bind b0) u0) z1 t4)))))))
1473 (sn3 c t3) (\lambda (x1: T).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4:
1474 T).(\lambda (H14: (eq T (THead (Bind b) t1 x0) (THead (Bind Abst) x1
1475 x2))).(\lambda (H15: (eq T t3 (THead (Bind Abbr) x3 x4))).(\lambda (_: (pr2 c
1476 x x3)).(\lambda (H17: ((\forall (b0: B).(\forall (u0: T).(pr2 (CHead c (Bind
1477 b0) u0) x2 x4))))).(let H18 \def (eq_ind T t3 (\lambda (t0: T).((eq T (THead
1478 (Flat Appl) x (THead (Bind b) t1 x0)) t0) \to (\forall (P: Prop).P))) H10
1479 (THead (Bind Abbr) x3 x4) H15) in (eq_ind_r T (THead (Bind Abbr) x3 x4)
1480 (\lambda (t0: T).(sn3 c t0)) (let H19 \def (f_equal T B (\lambda (e:
1481 T).(match e with [(TSort _) \Rightarrow b | (TLRef _) \Rightarrow b | (THead
1482 k _ _) \Rightarrow (match k with [(Bind b0) \Rightarrow b0 | (Flat _)
1483 \Rightarrow b])])) (THead (Bind b) t1 x0) (THead (Bind Abst) x1 x2) H14) in
1484 ((let H20 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
1485 \Rightarrow t1 | (TLRef _) \Rightarrow t1 | (THead _ t0 _) \Rightarrow t0]))
1486 (THead (Bind b) t1 x0) (THead (Bind Abst) x1 x2) H14) in ((let H21 \def
1487 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow x0 | (TLRef
1488 _) \Rightarrow x0 | (THead _ _ t0) \Rightarrow t0])) (THead (Bind b) t1 x0)
1489 (THead (Bind Abst) x1 x2) H14) in (\lambda (_: (eq T t1 x1)).(\lambda (H23:
1490 (eq B b Abst)).(let H24 \def (eq_ind_r T x2 (\lambda (t0: T).(\forall (b0:
1491 B).(\forall (u0: T).(pr2 (CHead c (Bind b0) u0) t0 x4)))) H17 x0 H21) in (let
1492 H25 \def (eq_ind B b (\lambda (b0: B).((eq T (THead (Flat Appl) x (THead
1493 (Bind b0) t1 x0)) (THead (Bind Abbr) x3 x4)) \to (\forall (P: Prop).P))) H18
1494 Abst H23) in (let H26 \def (eq_ind B b (\lambda (b0: B).(\forall (t4:
1495 T).((((eq T (THead (Flat Appl) (lift (S O) O x) x0) t4) \to (\forall (P:
1496 Prop).P))) \to ((pr3 (CHead c (Bind b0) t1) (THead (Flat Appl) (lift (S O) O
1497 x) x0) t4) \to (sn3 (CHead c (Bind b0) t1) t4))))) H9 Abst H23) in (let H27
1498 \def (eq_ind B b (\lambda (b0: B).(\forall (t4: T).((((eq T (THead (Flat
1499 Appl) (lift (S O) O x) x0) t4) \to (\forall (P: Prop).P))) \to ((pr3 (CHead c
1500 (Bind b0) t1) (THead (Flat Appl) (lift (S O) O x) x0) t4) \to (\forall (x5:
1501 T).(\forall (x6: T).((eq T t4 (THead (Flat Appl) (lift (S O) O x5) x6)) \to
1502 (sn3 c (THead (Flat Appl) x5 (THead (Bind b0) t1 x6)))))))))) H8 Abst H23) in
1503 (let H28 \def (eq_ind B b (\lambda (b0: B).(\forall (t4: T).((((eq T t1 t4)
1504 \to (\forall (P: Prop).P))) \to ((pr3 c t1 t4) \to (\forall (t0: T).(\forall
1505 (v0: T).((sn3 (CHead c (Bind b0) t4) (THead (Flat Appl) (lift (S O) O v0)
1506 t0)) \to (sn3 c (THead (Flat Appl) v0 (THead (Bind b0) t4 t0)))))))))) H2
1507 Abst H23) in (let H29 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0 Abst)))
1508 H Abst H23) in (let H30 \def (match (H29 (refl_equal B Abst)) in False with
1509 []) in H30)))))))))) H20)) H19)) t3 H15)))))))))) H13)) (\lambda (H13: (ex6_6
1510 B T T T T T (\lambda (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1511 T).(\lambda (_: T).(\lambda (_: T).(not (eq B b0 Abst)))))))) (\lambda (b0:
1512 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1513 (_: T).(eq T (THead (Bind b) t1 x0) (THead (Bind b0) y1 z1)))))))) (\lambda
1514 (b0: B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2:
1515 T).(\lambda (y2: T).(eq T t3 (THead (Bind b0) y2 (THead (Flat Appl) (lift (S
1516 O) O u2) z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda
1517 (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_:
1518 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1519 (y2: T).(pr2 c y1 y2))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (z1:
1520 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b0)
1521 y2) z1 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b0: B).(\lambda (_:
1522 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B
1523 b0 Abst)))))))) (\lambda (b0: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda
1524 (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Bind b) t1 x0) (THead
1525 (Bind b0) y1 z1)))))))) (\lambda (b0: B).(\lambda (_: T).(\lambda (_:
1526 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t3 (THead (Bind
1527 b0) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
1528 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1529 (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1530 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
1531 (\lambda (b0: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1532 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b0) y2) z1 z2))))))) (sn3 c t3)
1533 (\lambda (x1: B).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda
1534 (x5: T).(\lambda (x6: T).(\lambda (_: (not (eq B x1 Abst))).(\lambda (H15:
1535 (eq T (THead (Bind b) t1 x0) (THead (Bind x1) x2 x3))).(\lambda (H16: (eq T
1536 t3 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4)))).(\lambda
1537 (H17: (pr2 c x x5)).(\lambda (H18: (pr2 c x2 x6)).(\lambda (H19: (pr2 (CHead
1538 c (Bind x1) x6) x3 x4)).(let H20 \def (eq_ind T t3 (\lambda (t0: T).((eq T
1539 (THead (Flat Appl) x (THead (Bind b) t1 x0)) t0) \to (\forall (P: Prop).P)))
1540 H10 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4)) H16) in
1541 (eq_ind_r T (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
1542 (\lambda (t0: T).(sn3 c t0)) (let H21 \def (f_equal T B (\lambda (e:
1543 T).(match e with [(TSort _) \Rightarrow b | (TLRef _) \Rightarrow b | (THead
1544 k _ _) \Rightarrow (match k with [(Bind b0) \Rightarrow b0 | (Flat _)
1545 \Rightarrow b])])) (THead (Bind b) t1 x0) (THead (Bind x1) x2 x3) H15) in
1546 ((let H22 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _)
1547 \Rightarrow t1 | (TLRef _) \Rightarrow t1 | (THead _ t0 _) \Rightarrow t0]))
1548 (THead (Bind b) t1 x0) (THead (Bind x1) x2 x3) H15) in ((let H23 \def
1549 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow x0 | (TLRef
1550 _) \Rightarrow x0 | (THead _ _ t0) \Rightarrow t0])) (THead (Bind b) t1 x0)
1551 (THead (Bind x1) x2 x3) H15) in (\lambda (H24: (eq T t1 x2)).(\lambda (H25:
1552 (eq B b x1)).(let H26 \def (eq_ind_r T x3 (\lambda (t0: T).(pr2 (CHead c
1553 (Bind x1) x6) t0 x4)) H19 x0 H23) in (let H27 \def (eq_ind_r T x2 (\lambda
1554 (t0: T).(pr2 c t0 x6)) H18 t1 H24) in (let H28 \def (eq_ind_r B x1 (\lambda
1555 (b0: B).(pr2 (CHead c (Bind b0) x6) x0 x4)) H26 b H25) in (eq_ind B b
1556 (\lambda (b0: B).(sn3 c (THead (Bind b0) x6 (THead (Flat Appl) (lift (S O) O
1557 x5) x4)))) (sn3_pr3_trans c (THead (Bind b) t1 (THead (Flat Appl) (lift (S O)
1558 O x5) x4)) (sn3_bind b c t1 (sn3_sing c t1 H1) (THead (Flat Appl) (lift (S O)
1559 O x5) x4) (let H_x \def (term_dec x x5) in (let H29 \def H_x in (or_ind (eq T
1560 x x5) ((eq T x x5) \to (\forall (P: Prop).P)) (sn3 (CHead c (Bind b) t1)
1561 (THead (Flat Appl) (lift (S O) O x5) x4)) (\lambda (H30: (eq T x x5)).(let
1562 H31 \def (eq_ind_r T x5 (\lambda (t0: T).(pr2 c x t0)) H17 x H30) in (eq_ind
1563 T x (\lambda (t0: T).(sn3 (CHead c (Bind b) t1) (THead (Flat Appl) (lift (S
1564 O) O t0) x4))) (let H_x0 \def (term_dec x0 x4) in (let H32 \def H_x0 in
1565 (or_ind (eq T x0 x4) ((eq T x0 x4) \to (\forall (P: Prop).P)) (sn3 (CHead c
1566 (Bind b) t1) (THead (Flat Appl) (lift (S O) O x) x4)) (\lambda (H33: (eq T x0
1567 x4)).(let H34 \def (eq_ind_r T x4 (\lambda (t0: T).(pr2 (CHead c (Bind b) x6)
1568 x0 t0)) H28 x0 H33) in (eq_ind T x0 (\lambda (t0: T).(sn3 (CHead c (Bind b)
1569 t1) (THead (Flat Appl) (lift (S O) O x) t0))) (sn3_sing (CHead c (Bind b) t1)
1570 (THead (Flat Appl) (lift (S O) O x) x0) H9) x4 H33))) (\lambda (H33: (((eq T
1571 x0 x4) \to (\forall (P: Prop).P)))).(H9 (THead (Flat Appl) (lift (S O) O x)
1572 x4) (\lambda (H34: (eq T (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat
1573 Appl) (lift (S O) O x) x4))).(\lambda (P: Prop).(let H35 \def (f_equal T T
1574 (\lambda (e: T).(match e with [(TSort _) \Rightarrow x0 | (TLRef _)
1575 \Rightarrow x0 | (THead _ _ t0) \Rightarrow t0])) (THead (Flat Appl) (lift (S
1576 O) O x) x0) (THead (Flat Appl) (lift (S O) O x) x4) H34) in (let H36 \def
1577 (eq_ind_r T x4 (\lambda (t0: T).((eq T x0 t0) \to (\forall (P0: Prop).P0)))
1578 H33 x0 H35) in (let H37 \def (eq_ind_r T x4 (\lambda (t0: T).(pr2 (CHead c
1579 (Bind b) x6) x0 t0)) H28 x0 H35) in (H36 (refl_equal T x0) P))))))
1580 (pr3_pr3_pr3_t c t1 x6 (pr3_pr2 c t1 x6 H27) (THead (Flat Appl) (lift (S O) O
1581 x) x0) (THead (Flat Appl) (lift (S O) O x) x4) (Bind b) (pr3_pr2 (CHead c
1582 (Bind b) x6) (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat Appl) (lift
1583 (S O) O x) x4) (pr2_thin_dx (CHead c (Bind b) x6) x0 x4 H28 (lift (S O) O x)
1584 Appl))))) H32))) x5 H30))) (\lambda (H30: (((eq T x x5) \to (\forall (P:
1585 Prop).P)))).(H9 (THead (Flat Appl) (lift (S O) O x5) x4) (\lambda (H31: (eq T
1586 (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat Appl) (lift (S O) O x5)
1587 x4))).(\lambda (P: Prop).(let H32 \def (f_equal T T (\lambda (e: T).(match e
1588 with [(TSort _) \Rightarrow (lref_map (\lambda (x7: nat).(plus x7 (S O))) O
1589 x) | (TLRef _) \Rightarrow (lref_map (\lambda (x7: nat).(plus x7 (S O))) O x)
1590 | (THead _ t0 _) \Rightarrow t0])) (THead (Flat Appl) (lift (S O) O x) x0)
1591 (THead (Flat Appl) (lift (S O) O x5) x4) H31) in ((let H33 \def (f_equal T T
1592 (\lambda (e: T).(match e with [(TSort _) \Rightarrow x0 | (TLRef _)
1593 \Rightarrow x0 | (THead _ _ t0) \Rightarrow t0])) (THead (Flat Appl) (lift (S
1594 O) O x) x0) (THead (Flat Appl) (lift (S O) O x5) x4) H31) in (\lambda (H34:
1595 (eq T (lift (S O) O x) (lift (S O) O x5))).(let H35 \def (eq_ind_r T x5
1596 (\lambda (t0: T).((eq T x t0) \to (\forall (P0: Prop).P0))) H30 x (lift_inj x
1597 x5 (S O) O H34)) in (let H36 \def (eq_ind_r T x5 (\lambda (t0: T).(pr2 c x
1598 t0)) H17 x (lift_inj x x5 (S O) O H34)) in (let H37 \def (eq_ind_r T x4
1599 (\lambda (t0: T).(pr2 (CHead c (Bind b) x6) x0 t0)) H28 x0 H33) in (H35
1600 (refl_equal T x) P)))))) H32)))) (pr3_pr3_pr3_t c t1 x6 (pr3_pr2 c t1 x6 H27)
1601 (THead (Flat Appl) (lift (S O) O x) x0) (THead (Flat Appl) (lift (S O) O x5)
1602 x4) (Bind b) (pr3_flat (CHead c (Bind b) x6) (lift (S O) O x) (lift (S O) O
1603 x5) (pr3_lift (CHead c (Bind b) x6) c (S O) O (drop_drop (Bind b) O c c
1604 (drop_refl c) x6) x x5 (pr3_pr2 c x x5 H17)) x0 x4 (pr3_pr2 (CHead c (Bind b)
1605 x6) x0 x4 H28) Appl)))) H29)))) (THead (Bind b) x6 (THead (Flat Appl) (lift
1606 (S O) O x5) x4)) (pr3_pr2 c (THead (Bind b) t1 (THead (Flat Appl) (lift (S O)
1607 O x5) x4)) (THead (Bind b) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
1608 (pr2_head_1 c t1 x6 H27 (Bind b) (THead (Flat Appl) (lift (S O) O x5) x4))))
1609 x1 H25))))))) H22)) H21)) t3 H16)))))))))))))) H13)) H12)))))))))))))) y
1610 H4))))) H3))))))) u H0))))).
1612 theorem sn3_appl_appl:
1613 \forall (v1: T).(\forall (t1: T).(let u1 \def (THead (Flat Appl) v1 t1) in
1614 (\forall (c: C).((sn3 c u1) \to (\forall (v2: T).((sn3 c v2) \to (((\forall
1615 (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2) \to (\forall (P: Prop).P))) \to
1616 (sn3 c (THead (Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2
1619 \lambda (v1: T).(\lambda (t1: T).(let u1 \def (THead (Flat Appl) v1 t1) in
1620 (\lambda (c: C).(\lambda (H: (sn3 c (THead (Flat Appl) v1 t1))).(insert_eq T
1621 (THead (Flat Appl) v1 t1) (\lambda (t: T).(sn3 c t)) (\lambda (t: T).(\forall
1622 (v2: T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c t u2) \to ((((iso t u2)
1623 \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to
1624 (sn3 c (THead (Flat Appl) v2 t)))))) (\lambda (y: T).(\lambda (H0: (sn3 c
1625 y)).(unintro T t1 (\lambda (t: T).((eq T y (THead (Flat Appl) v1 t)) \to
1626 (\forall (v2: T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c y u2) \to ((((iso
1627 y u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2))))))
1628 \to (sn3 c (THead (Flat Appl) v2 y))))))) (unintro T v1 (\lambda (t:
1629 T).(\forall (x: T).((eq T y (THead (Flat Appl) t x)) \to (\forall (v2:
1630 T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c y u2) \to ((((iso y u2) \to
1631 (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to (sn3 c
1632 (THead (Flat Appl) v2 y)))))))) (sn3_ind c (\lambda (t: T).(\forall (x:
1633 T).(\forall (x0: T).((eq T t (THead (Flat Appl) x x0)) \to (\forall (v2:
1634 T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c t u2) \to ((((iso t u2) \to
1635 (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to (sn3 c
1636 (THead (Flat Appl) v2 t))))))))) (\lambda (t2: T).(\lambda (H1: ((\forall
1637 (t3: T).((((eq T t2 t3) \to (\forall (P: Prop).P))) \to ((pr3 c t2 t3) \to
1638 (sn3 c t3)))))).(\lambda (H2: ((\forall (t3: T).((((eq T t2 t3) \to (\forall
1639 (P: Prop).P))) \to ((pr3 c t2 t3) \to (\forall (x: T).(\forall (x0: T).((eq T
1640 t3 (THead (Flat Appl) x x0)) \to (\forall (v2: T).((sn3 c v2) \to (((\forall
1641 (u2: T).((pr3 c t3 u2) \to ((((iso t3 u2) \to (\forall (P: Prop).P))) \to
1642 (sn3 c (THead (Flat Appl) v2 u2)))))) \to (sn3 c (THead (Flat Appl) v2
1643 t3))))))))))))).(\lambda (x: T).(\lambda (x0: T).(\lambda (H3: (eq T t2
1644 (THead (Flat Appl) x x0))).(\lambda (v2: T).(\lambda (H4: (sn3 c
1645 v2)).(sn3_ind c (\lambda (t: T).(((\forall (u2: T).((pr3 c t2 u2) \to ((((iso
1646 t2 u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) t u2))))))
1647 \to (sn3 c (THead (Flat Appl) t t2)))) (\lambda (t0: T).(\lambda (H5:
1648 ((\forall (t3: T).((((eq T t0 t3) \to (\forall (P: Prop).P))) \to ((pr3 c t0
1649 t3) \to (sn3 c t3)))))).(\lambda (H6: ((\forall (t3: T).((((eq T t0 t3) \to
1650 (\forall (P: Prop).P))) \to ((pr3 c t0 t3) \to (((\forall (u2: T).((pr3 c t2
1651 u2) \to ((((iso t2 u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat
1652 Appl) t3 u2)))))) \to (sn3 c (THead (Flat Appl) t3 t2)))))))).(\lambda (H7:
1653 ((\forall (u2: T).((pr3 c t2 u2) \to ((((iso t2 u2) \to (\forall (P:
1654 Prop).P))) \to (sn3 c (THead (Flat Appl) t0 u2))))))).(let H8 \def (eq_ind T
1655 t2 (\lambda (t: T).(\forall (u2: T).((pr3 c t u2) \to ((((iso t u2) \to
1656 (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) t0 u2)))))) H7 (THead
1657 (Flat Appl) x x0) H3) in (let H9 \def (eq_ind T t2 (\lambda (t: T).(\forall
1658 (t3: T).((((eq T t0 t3) \to (\forall (P: Prop).P))) \to ((pr3 c t0 t3) \to
1659 (((\forall (u2: T).((pr3 c t u2) \to ((((iso t u2) \to (\forall (P:
1660 Prop).P))) \to (sn3 c (THead (Flat Appl) t3 u2)))))) \to (sn3 c (THead (Flat
1661 Appl) t3 t))))))) H6 (THead (Flat Appl) x x0) H3) in (let H10 \def (eq_ind T
1662 t2 (\lambda (t: T).(\forall (t3: T).((((eq T t t3) \to (\forall (P:
1663 Prop).P))) \to ((pr3 c t t3) \to (\forall (x1: T).(\forall (x2: T).((eq T t3
1664 (THead (Flat Appl) x1 x2)) \to (\forall (v3: T).((sn3 c v3) \to (((\forall
1665 (u2: T).((pr3 c t3 u2) \to ((((iso t3 u2) \to (\forall (P: Prop).P))) \to
1666 (sn3 c (THead (Flat Appl) v3 u2)))))) \to (sn3 c (THead (Flat Appl) v3
1667 t3)))))))))))) H2 (THead (Flat Appl) x x0) H3) in (let H11 \def (eq_ind T t2
1668 (\lambda (t: T).(\forall (t3: T).((((eq T t t3) \to (\forall (P: Prop).P)))
1669 \to ((pr3 c t t3) \to (sn3 c t3))))) H1 (THead (Flat Appl) x x0) H3) in
1670 (eq_ind_r T (THead (Flat Appl) x x0) (\lambda (t: T).(sn3 c (THead (Flat
1671 Appl) t0 t))) (sn3_pr2_intro c (THead (Flat Appl) t0 (THead (Flat Appl) x
1672 x0)) (\lambda (t3: T).(\lambda (H12: (((eq T (THead (Flat Appl) t0 (THead
1673 (Flat Appl) x x0)) t3) \to (\forall (P: Prop).P)))).(\lambda (H13: (pr2 c
1674 (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t3)).(let H14 \def
1675 (pr2_gen_appl c t0 (THead (Flat Appl) x x0) t3 H13) in (or3_ind (ex3_2 T T
1676 (\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 t4))))
1677 (\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2))) (\lambda (_: T).(\lambda
1678 (t4: T).(pr2 c (THead (Flat Appl) x x0) t4)))) (ex4_4 T T T T (\lambda (y1:
1679 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Appl)
1680 x x0) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda
1681 (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
1682 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2)))))
1683 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall
1684 (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4)))))))) (ex6_6 B T T T
1685 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1686 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
1687 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq
1688 T (THead (Flat Appl) x x0) (THead (Bind b) y1 z1)))))))) (\lambda (b:
1689 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
1690 (y2: T).(eq T t3 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2)
1691 z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1692 T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2))))))) (\lambda (_:
1693 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1694 (y2: T).(pr2 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
1695 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b)
1696 y2) z1 z2)))))))) (sn3 c t3) (\lambda (H15: (ex3_2 T T (\lambda (u2:
1697 T).(\lambda (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2:
1698 T).(\lambda (_: T).(pr2 c t0 u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c
1699 (THead (Flat Appl) x x0) t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda
1700 (t4: T).(eq T t3 (THead (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_:
1701 T).(pr2 c t0 u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c (THead (Flat Appl)
1702 x x0) t4))) (sn3 c t3) (\lambda (x1: T).(\lambda (x2: T).(\lambda (H16: (eq T
1703 t3 (THead (Flat Appl) x1 x2))).(\lambda (H17: (pr2 c t0 x1)).(\lambda (H18:
1704 (pr2 c (THead (Flat Appl) x x0) x2)).(let H19 \def (eq_ind T t3 (\lambda (t:
1705 T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t) \to (\forall (P:
1706 Prop).P))) H12 (THead (Flat Appl) x1 x2) H16) in (eq_ind_r T (THead (Flat
1707 Appl) x1 x2) (\lambda (t: T).(sn3 c t)) (let H20 \def (pr2_gen_appl c x x0 x2
1708 H18) in (or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t4: T).(eq T x2 (THead
1709 (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
1710 (\lambda (_: T).(\lambda (t4: T).(pr2 c x0 t4)))) (ex4_4 T T T T (\lambda
1711 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T x0 (THead
1712 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1713 T).(\lambda (t4: T).(eq T x2 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
1714 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
1715 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b:
1716 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4)))))))) (ex6_6 B T T T T T
1717 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1718 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
1719 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T x0
1720 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
1721 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T x2 (THead (Bind
1722 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
1723 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1724 (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1725 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
1726 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1727 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))) (sn3 c
1728 (THead (Flat Appl) x1 x2)) (\lambda (H21: (ex3_2 T T (\lambda (u2:
1729 T).(\lambda (t4: T).(eq T x2 (THead (Flat Appl) u2 t4)))) (\lambda (u2:
1730 T).(\lambda (_: T).(pr2 c x u2))) (\lambda (_: T).(\lambda (t4: T).(pr2 c x0
1731 t4))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t4: T).(eq T x2 (THead
1732 (Flat Appl) u2 t4)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))
1733 (\lambda (_: T).(\lambda (t4: T).(pr2 c x0 t4))) (sn3 c (THead (Flat Appl) x1
1734 x2)) (\lambda (x3: T).(\lambda (x4: T).(\lambda (H22: (eq T x2 (THead (Flat
1735 Appl) x3 x4))).(\lambda (H23: (pr2 c x x3)).(\lambda (H24: (pr2 c x0
1736 x4)).(let H25 \def (eq_ind T x2 (\lambda (t: T).((eq T (THead (Flat Appl) t0
1737 (THead (Flat Appl) x x0)) (THead (Flat Appl) x1 t)) \to (\forall (P:
1738 Prop).P))) H19 (THead (Flat Appl) x3 x4) H22) in (eq_ind_r T (THead (Flat
1739 Appl) x3 x4) (\lambda (t: T).(sn3 c (THead (Flat Appl) x1 t))) (let H_x \def
1740 (term_dec (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4)) in (let H26
1741 \def H_x in (or_ind (eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4))
1742 ((eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4)) \to (\forall (P:
1743 Prop).P)) (sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x3 x4))) (\lambda
1744 (H27: (eq T (THead (Flat Appl) x x0) (THead (Flat Appl) x3 x4))).(let H28
1745 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow x |
1746 (TLRef _) \Rightarrow x | (THead _ t _) \Rightarrow t])) (THead (Flat Appl) x
1747 x0) (THead (Flat Appl) x3 x4) H27) in ((let H29 \def (f_equal T T (\lambda
1748 (e: T).(match e with [(TSort _) \Rightarrow x0 | (TLRef _) \Rightarrow x0 |
1749 (THead _ _ t) \Rightarrow t])) (THead (Flat Appl) x x0) (THead (Flat Appl) x3
1750 x4) H27) in (\lambda (H30: (eq T x x3)).(let H31 \def (eq_ind_r T x4 (\lambda
1751 (t: T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) (THead (Flat
1752 Appl) x1 (THead (Flat Appl) x3 t))) \to (\forall (P: Prop).P))) H25 x0 H29)
1753 in (let H32 \def (eq_ind_r T x4 (\lambda (t: T).(pr2 c x0 t)) H24 x0 H29) in
1754 (eq_ind T x0 (\lambda (t: T).(sn3 c (THead (Flat Appl) x1 (THead (Flat Appl)
1755 x3 t)))) (let H33 \def (eq_ind_r T x3 (\lambda (t: T).((eq T (THead (Flat
1756 Appl) t0 (THead (Flat Appl) x x0)) (THead (Flat Appl) x1 (THead (Flat Appl) t
1757 x0))) \to (\forall (P: Prop).P))) H31 x H30) in (let H34 \def (eq_ind_r T x3
1758 (\lambda (t: T).(pr2 c x t)) H23 x H30) in (eq_ind T x (\lambda (t: T).(sn3 c
1759 (THead (Flat Appl) x1 (THead (Flat Appl) t x0)))) (let H_x0 \def (term_dec t0
1760 x1) in (let H35 \def H_x0 in (or_ind (eq T t0 x1) ((eq T t0 x1) \to (\forall
1761 (P: Prop).P)) (sn3 c (THead (Flat Appl) x1 (THead (Flat Appl) x x0)))
1762 (\lambda (H36: (eq T t0 x1)).(let H37 \def (eq_ind_r T x1 (\lambda (t:
1763 T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) (THead (Flat Appl)
1764 t (THead (Flat Appl) x x0))) \to (\forall (P: Prop).P))) H33 t0 H36) in (let
1765 H38 \def (eq_ind_r T x1 (\lambda (t: T).(pr2 c t0 t)) H17 t0 H36) in (eq_ind
1766 T t0 (\lambda (t: T).(sn3 c (THead (Flat Appl) t (THead (Flat Appl) x x0))))
1767 (H37 (refl_equal T (THead (Flat Appl) t0 (THead (Flat Appl) x x0))) (sn3 c
1768 (THead (Flat Appl) t0 (THead (Flat Appl) x x0)))) x1 H36)))) (\lambda (H36:
1769 (((eq T t0 x1) \to (\forall (P: Prop).P)))).(H9 x1 H36 (pr3_pr2 c t0 x1 H17)
1770 (\lambda (u2: T).(\lambda (H37: (pr3 c (THead (Flat Appl) x x0) u2)).(\lambda
1771 (H38: (((iso (THead (Flat Appl) x x0) u2) \to (\forall (P:
1772 Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t0 u2) (H8 u2 H37 H38) (THead
1773 (Flat Appl) x1 u2) (pr3_pr2 c (THead (Flat Appl) t0 u2) (THead (Flat Appl) x1
1774 u2) (pr2_head_1 c t0 x1 H17 (Flat Appl) u2)))))))) H35))) x3 H30))) x4
1775 H29))))) H28))) (\lambda (H27: (((eq T (THead (Flat Appl) x x0) (THead (Flat
1776 Appl) x3 x4)) \to (\forall (P: Prop).P)))).(H10 (THead (Flat Appl) x3 x4) H27
1777 (pr3_flat c x x3 (pr3_pr2 c x x3 H23) x0 x4 (pr3_pr2 c x0 x4 H24) Appl) x3 x4
1778 (refl_equal T (THead (Flat Appl) x3 x4)) x1 (sn3_pr3_trans c t0 (sn3_sing c
1779 t0 H5) x1 (pr3_pr2 c t0 x1 H17)) (\lambda (u2: T).(\lambda (H28: (pr3 c
1780 (THead (Flat Appl) x3 x4) u2)).(\lambda (H29: (((iso (THead (Flat Appl) x3
1781 x4) u2) \to (\forall (P: Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t0
1782 u2) (H8 u2 (pr3_sing c (THead (Flat Appl) x x4) (THead (Flat Appl) x x0)
1783 (pr2_thin_dx c x0 x4 H24 x Appl) u2 (pr3_sing c (THead (Flat Appl) x3 x4)
1784 (THead (Flat Appl) x x4) (pr2_head_1 c x x3 H23 (Flat Appl) x4) u2 H28))
1785 (\lambda (H30: (iso (THead (Flat Appl) x x0) u2)).(\lambda (P: Prop).(H29
1786 (iso_trans (THead (Flat Appl) x3 x4) (THead (Flat Appl) x x0) (iso_head x3 x
1787 x4 x0 (Flat Appl)) u2 H30) P)))) (THead (Flat Appl) x1 u2) (pr3_pr2 c (THead
1788 (Flat Appl) t0 u2) (THead (Flat Appl) x1 u2) (pr2_head_1 c t0 x1 H17 (Flat
1789 Appl) u2)))))))) H26))) x2 H22))))))) H21)) (\lambda (H21: (ex4_4 T T T T
1790 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T x0
1791 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1792 T).(\lambda (t4: T).(eq T x2 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
1793 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
1794 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b:
1795 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4))))))))).(ex4_4_ind T T T
1796 T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T x0
1797 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1798 T).(\lambda (t4: T).(eq T x2 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
1799 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2))))) (\lambda
1800 (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall (b:
1801 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4))))))) (sn3 c (THead (Flat
1802 Appl) x1 x2)) (\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda
1803 (x6: T).(\lambda (H22: (eq T x0 (THead (Bind Abst) x3 x4))).(\lambda (H23:
1804 (eq T x2 (THead (Bind Abbr) x5 x6))).(\lambda (H24: (pr2 c x x5)).(\lambda
1805 (H25: ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x4
1806 x6))))).(let H26 \def (eq_ind T x2 (\lambda (t: T).((eq T (THead (Flat Appl)
1807 t0 (THead (Flat Appl) x x0)) (THead (Flat Appl) x1 t)) \to (\forall (P:
1808 Prop).P))) H19 (THead (Bind Abbr) x5 x6) H23) in (eq_ind_r T (THead (Bind
1809 Abbr) x5 x6) (\lambda (t: T).(sn3 c (THead (Flat Appl) x1 t))) (let H27 \def
1810 (eq_ind T x0 (\lambda (t: T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl)
1811 x t)) (THead (Flat Appl) x1 (THead (Bind Abbr) x5 x6))) \to (\forall (P:
1812 Prop).P))) H26 (THead (Bind Abst) x3 x4) H22) in (let H28 \def (eq_ind T x0
1813 (\lambda (t: T).(\forall (t4: T).((((eq T (THead (Flat Appl) x t) t4) \to
1814 (\forall (P: Prop).P))) \to ((pr3 c (THead (Flat Appl) x t) t4) \to (sn3 c
1815 t4))))) H11 (THead (Bind Abst) x3 x4) H22) in (let H29 \def (eq_ind T x0
1816 (\lambda (t: T).(\forall (t4: T).((((eq T (THead (Flat Appl) x t) t4) \to
1817 (\forall (P: Prop).P))) \to ((pr3 c (THead (Flat Appl) x t) t4) \to (\forall
1818 (x7: T).(\forall (x8: T).((eq T t4 (THead (Flat Appl) x7 x8)) \to (\forall
1819 (v3: T).((sn3 c v3) \to (((\forall (u2: T).((pr3 c t4 u2) \to ((((iso t4 u2)
1820 \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v3 u2)))))) \to
1821 (sn3 c (THead (Flat Appl) v3 t4)))))))))))) H10 (THead (Bind Abst) x3 x4)
1822 H22) in (let H30 \def (eq_ind T x0 (\lambda (t: T).(\forall (u2: T).((pr3 c
1823 (THead (Flat Appl) x t) u2) \to ((((iso (THead (Flat Appl) x t) u2) \to
1824 (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) t0 u2)))))) H8 (THead
1825 (Bind Abst) x3 x4) H22) in (let H31 \def (eq_ind T x0 (\lambda (t:
1826 T).(\forall (t4: T).((((eq T t0 t4) \to (\forall (P: Prop).P))) \to ((pr3 c
1827 t0 t4) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x t) u2) \to ((((iso
1828 (THead (Flat Appl) x t) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead
1829 (Flat Appl) t4 u2)))))) \to (sn3 c (THead (Flat Appl) t4 (THead (Flat Appl) x
1830 t)))))))) H9 (THead (Bind Abst) x3 x4) H22) in (sn3_pr3_trans c (THead (Flat
1831 Appl) t0 (THead (Bind Abbr) x5 x6)) (H30 (THead (Bind Abbr) x5 x6) (pr3_sing
1832 c (THead (Bind Abbr) x x4) (THead (Flat Appl) x (THead (Bind Abst) x3 x4))
1833 (pr2_free c (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) (THead (Bind
1834 Abbr) x x4) (pr0_beta x3 x x (pr0_refl x) x4 x4 (pr0_refl x4))) (THead (Bind
1835 Abbr) x5 x6) (pr3_head_12 c x x5 (pr3_pr2 c x x5 H24) (Bind Abbr) x4 x6
1836 (pr3_pr2 (CHead c (Bind Abbr) x5) x4 x6 (H25 Abbr x5)))) (\lambda (H32: (iso
1837 (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) (THead (Bind Abbr) x5
1838 x6))).(\lambda (P: Prop).(let H33 \def (match H32 with [(iso_sort n1 n2)
1839 \Rightarrow (\lambda (H33: (eq T (TSort n1) (THead (Flat Appl) x (THead (Bind
1840 Abst) x3 x4)))).(\lambda (H34: (eq T (TSort n2) (THead (Bind Abbr) x5
1841 x6))).((let H35 \def (eq_ind T (TSort n1) (\lambda (e: T).(match e with
1842 [(TSort _) \Rightarrow True | (TLRef _) \Rightarrow False | (THead _ _ _)
1843 \Rightarrow False])) I (THead (Flat Appl) x (THead (Bind Abst) x3 x4)) H33)
1844 in (False_ind ((eq T (TSort n2) (THead (Bind Abbr) x5 x6)) \to P) H35))
1845 H34))) | (iso_lref i1 i2) \Rightarrow (\lambda (H33: (eq T (TLRef i1) (THead
1846 (Flat Appl) x (THead (Bind Abst) x3 x4)))).(\lambda (H34: (eq T (TLRef i2)
1847 (THead (Bind Abbr) x5 x6))).((let H35 \def (eq_ind T (TLRef i1) (\lambda (e:
1848 T).(match e with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow True |
1849 (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) x (THead (Bind Abst)
1850 x3 x4)) H33) in (False_ind ((eq T (TLRef i2) (THead (Bind Abbr) x5 x6)) \to
1851 P) H35)) H34))) | (iso_head v4 v5 t4 t5 k) \Rightarrow (\lambda (H33: (eq T
1852 (THead k v4 t4) (THead (Flat Appl) x (THead (Bind Abst) x3 x4)))).(\lambda
1853 (H34: (eq T (THead k v5 t5) (THead (Bind Abbr) x5 x6))).((let H35 \def
1854 (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t4 | (TLRef
1855 _) \Rightarrow t4 | (THead _ _ t) \Rightarrow t])) (THead k v4 t4) (THead
1856 (Flat Appl) x (THead (Bind Abst) x3 x4)) H33) in ((let H36 \def (f_equal T T
1857 (\lambda (e: T).(match e with [(TSort _) \Rightarrow v4 | (TLRef _)
1858 \Rightarrow v4 | (THead _ t _) \Rightarrow t])) (THead k v4 t4) (THead (Flat
1859 Appl) x (THead (Bind Abst) x3 x4)) H33) in ((let H37 \def (f_equal T K
1860 (\lambda (e: T).(match e with [(TSort _) \Rightarrow k | (TLRef _)
1861 \Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k v4 t4) (THead (Flat
1862 Appl) x (THead (Bind Abst) x3 x4)) H33) in (eq_ind K (Flat Appl) (\lambda
1863 (k0: K).((eq T v4 x) \to ((eq T t4 (THead (Bind Abst) x3 x4)) \to ((eq T
1864 (THead k0 v5 t5) (THead (Bind Abbr) x5 x6)) \to P)))) (\lambda (H38: (eq T v4
1865 x)).(eq_ind T x (\lambda (_: T).((eq T t4 (THead (Bind Abst) x3 x4)) \to ((eq
1866 T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5 x6)) \to P))) (\lambda
1867 (H39: (eq T t4 (THead (Bind Abst) x3 x4))).(eq_ind T (THead (Bind Abst) x3
1868 x4) (\lambda (_: T).((eq T (THead (Flat Appl) v5 t5) (THead (Bind Abbr) x5
1869 x6)) \to P)) (\lambda (H40: (eq T (THead (Flat Appl) v5 t5) (THead (Bind
1870 Abbr) x5 x6))).(let H41 \def (eq_ind T (THead (Flat Appl) v5 t5) (\lambda (e:
1871 T).(match e with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False |
1872 (THead k0 _ _) \Rightarrow (match k0 with [(Bind _) \Rightarrow False | (Flat
1873 _) \Rightarrow True])])) I (THead (Bind Abbr) x5 x6) H40) in (False_ind P
1874 H41))) t4 (sym_eq T t4 (THead (Bind Abst) x3 x4) H39))) v4 (sym_eq T v4 x
1875 H38))) k (sym_eq K k (Flat Appl) H37))) H36)) H35)) H34)))]) in (H33
1876 (refl_equal T (THead (Flat Appl) x (THead (Bind Abst) x3 x4))) (refl_equal T
1877 (THead (Bind Abbr) x5 x6))))))) (THead (Flat Appl) x1 (THead (Bind Abbr) x5
1878 x6)) (pr3_pr2 c (THead (Flat Appl) t0 (THead (Bind Abbr) x5 x6)) (THead (Flat
1879 Appl) x1 (THead (Bind Abbr) x5 x6)) (pr2_head_1 c t0 x1 H17 (Flat Appl)
1880 (THead (Bind Abbr) x5 x6))))))))) x2 H23)))))))))) H21)) (\lambda (H21:
1881 (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
1882 (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
1883 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1884 (_: T).(eq T x0 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
1885 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
1886 x2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
1887 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1888 T).(\lambda (_: T).(pr2 c x u2))))))) (\lambda (_: B).(\lambda (y1:
1889 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
1890 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
1891 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1
1892 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda
1893 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b
1894 Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
1895 T).(\lambda (_: T).(\lambda (_: T).(eq T x0 (THead (Bind b) y1 z1))))))))
1896 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda
1897 (u2: T).(\lambda (y2: T).(eq T x2 (THead (Bind b) y2 (THead (Flat Appl) (lift
1898 (S O) O u2) z2))))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
1899 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x u2)))))))
1900 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1901 T).(\lambda (y2: T).(pr2 c y1 y2))))))) (\lambda (b: B).(\lambda (_:
1902 T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr2
1903 (CHead c (Bind b) y2) z1 z2))))))) (sn3 c (THead (Flat Appl) x1 x2)) (\lambda
1904 (x3: B).(\lambda (x4: T).(\lambda (x5: T).(\lambda (x6: T).(\lambda (x7:
1905 T).(\lambda (x8: T).(\lambda (H22: (not (eq B x3 Abst))).(\lambda (H23: (eq T
1906 x0 (THead (Bind x3) x4 x5))).(\lambda (H24: (eq T x2 (THead (Bind x3) x8
1907 (THead (Flat Appl) (lift (S O) O x7) x6)))).(\lambda (H25: (pr2 c x
1908 x7)).(\lambda (H26: (pr2 c x4 x8)).(\lambda (H27: (pr2 (CHead c (Bind x3) x8)
1909 x5 x6)).(let H28 \def (eq_ind T x2 (\lambda (t: T).((eq T (THead (Flat Appl)
1910 t0 (THead (Flat Appl) x x0)) (THead (Flat Appl) x1 t)) \to (\forall (P:
1911 Prop).P))) H19 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
1912 H24) in (eq_ind_r T (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7)
1913 x6)) (\lambda (t: T).(sn3 c (THead (Flat Appl) x1 t))) (let H29 \def (eq_ind
1914 T x0 (\lambda (t: T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x t))
1915 (THead (Flat Appl) x1 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O
1916 x7) x6)))) \to (\forall (P: Prop).P))) H28 (THead (Bind x3) x4 x5) H23) in
1917 (let H30 \def (eq_ind T x0 (\lambda (t: T).(\forall (t4: T).((((eq T (THead
1918 (Flat Appl) x t) t4) \to (\forall (P: Prop).P))) \to ((pr3 c (THead (Flat
1919 Appl) x t) t4) \to (sn3 c t4))))) H11 (THead (Bind x3) x4 x5) H23) in (let
1920 H31 \def (eq_ind T x0 (\lambda (t: T).(\forall (t4: T).((((eq T (THead (Flat
1921 Appl) x t) t4) \to (\forall (P: Prop).P))) \to ((pr3 c (THead (Flat Appl) x
1922 t) t4) \to (\forall (x9: T).(\forall (x10: T).((eq T t4 (THead (Flat Appl) x9
1923 x10)) \to (\forall (v3: T).((sn3 c v3) \to (((\forall (u2: T).((pr3 c t4 u2)
1924 \to ((((iso t4 u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl)
1925 v3 u2)))))) \to (sn3 c (THead (Flat Appl) v3 t4)))))))))))) H10 (THead (Bind
1926 x3) x4 x5) H23) in (let H32 \def (eq_ind T x0 (\lambda (t: T).(\forall (u2:
1927 T).((pr3 c (THead (Flat Appl) x t) u2) \to ((((iso (THead (Flat Appl) x t)
1928 u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) t0 u2)))))) H8
1929 (THead (Bind x3) x4 x5) H23) in (let H33 \def (eq_ind T x0 (\lambda (t:
1930 T).(\forall (t4: T).((((eq T t0 t4) \to (\forall (P: Prop).P))) \to ((pr3 c
1931 t0 t4) \to (((\forall (u2: T).((pr3 c (THead (Flat Appl) x t) u2) \to ((((iso
1932 (THead (Flat Appl) x t) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead
1933 (Flat Appl) t4 u2)))))) \to (sn3 c (THead (Flat Appl) t4 (THead (Flat Appl) x
1934 t)))))))) H9 (THead (Bind x3) x4 x5) H23) in (sn3_pr3_trans c (THead (Flat
1935 Appl) t0 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) (H32
1936 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)) (pr3_sing c
1937 (THead (Bind x3) x4 (THead (Flat Appl) (lift (S O) O x) x5)) (THead (Flat
1938 Appl) x (THead (Bind x3) x4 x5)) (pr2_free c (THead (Flat Appl) x (THead
1939 (Bind x3) x4 x5)) (THead (Bind x3) x4 (THead (Flat Appl) (lift (S O) O x)
1940 x5)) (pr0_upsilon x3 H22 x x (pr0_refl x) x4 x4 (pr0_refl x4) x5 x5 (pr0_refl
1941 x5))) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))
1942 (pr3_head_12 c x4 x8 (pr3_pr2 c x4 x8 H26) (Bind x3) (THead (Flat Appl) (lift
1943 (S O) O x) x5) (THead (Flat Appl) (lift (S O) O x7) x6) (pr3_head_12 (CHead c
1944 (Bind x3) x8) (lift (S O) O x) (lift (S O) O x7) (pr3_lift (CHead c (Bind x3)
1945 x8) c (S O) O (drop_drop (Bind x3) O c c (drop_refl c) x8) x x7 (pr3_pr2 c x
1946 x7 H25)) (Flat Appl) x5 x6 (pr3_pr2 (CHead (CHead c (Bind x3) x8) (Flat Appl)
1947 (lift (S O) O x7)) x5 x6 (pr2_cflat (CHead c (Bind x3) x8) x5 x6 H27 Appl
1948 (lift (S O) O x7)))))) (\lambda (H34: (iso (THead (Flat Appl) x (THead (Bind
1949 x3) x4 x5)) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7)
1950 x6)))).(\lambda (P: Prop).(let H35 \def (match H34 with [(iso_sort n1 n2)
1951 \Rightarrow (\lambda (H35: (eq T (TSort n1) (THead (Flat Appl) x (THead (Bind
1952 x3) x4 x5)))).(\lambda (H36: (eq T (TSort n2) (THead (Bind x3) x8 (THead
1953 (Flat Appl) (lift (S O) O x7) x6)))).((let H37 \def (eq_ind T (TSort n1)
1954 (\lambda (e: T).(match e with [(TSort _) \Rightarrow True | (TLRef _)
1955 \Rightarrow False | (THead _ _ _) \Rightarrow False])) I (THead (Flat Appl) x
1956 (THead (Bind x3) x4 x5)) H35) in (False_ind ((eq T (TSort n2) (THead (Bind
1957 x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to P) H37)) H36))) |
1958 (iso_lref i1 i2) \Rightarrow (\lambda (H35: (eq T (TLRef i1) (THead (Flat
1959 Appl) x (THead (Bind x3) x4 x5)))).(\lambda (H36: (eq T (TLRef i2) (THead
1960 (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)))).((let H37 \def
1961 (eq_ind T (TLRef i1) (\lambda (e: T).(match e with [(TSort _) \Rightarrow
1962 False | (TLRef _) \Rightarrow True | (THead _ _ _) \Rightarrow False])) I
1963 (THead (Flat Appl) x (THead (Bind x3) x4 x5)) H35) in (False_ind ((eq T
1964 (TLRef i2) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) \to
1965 P) H37)) H36))) | (iso_head v4 v5 t4 t5 k) \Rightarrow (\lambda (H35: (eq T
1966 (THead k v4 t4) (THead (Flat Appl) x (THead (Bind x3) x4 x5)))).(\lambda
1967 (H36: (eq T (THead k v5 t5) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S
1968 O) O x7) x6)))).((let H37 \def (f_equal T T (\lambda (e: T).(match e with
1969 [(TSort _) \Rightarrow t4 | (TLRef _) \Rightarrow t4 | (THead _ _ t)
1970 \Rightarrow t])) (THead k v4 t4) (THead (Flat Appl) x (THead (Bind x3) x4
1971 x5)) H35) in ((let H38 \def (f_equal T T (\lambda (e: T).(match e with
1972 [(TSort _) \Rightarrow v4 | (TLRef _) \Rightarrow v4 | (THead _ t _)
1973 \Rightarrow t])) (THead k v4 t4) (THead (Flat Appl) x (THead (Bind x3) x4
1974 x5)) H35) in ((let H39 \def (f_equal T K (\lambda (e: T).(match e with
1975 [(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _)
1976 \Rightarrow k0])) (THead k v4 t4) (THead (Flat Appl) x (THead (Bind x3) x4
1977 x5)) H35) in (eq_ind K (Flat Appl) (\lambda (k0: K).((eq T v4 x) \to ((eq T
1978 t4 (THead (Bind x3) x4 x5)) \to ((eq T (THead k0 v5 t5) (THead (Bind x3) x8
1979 (THead (Flat Appl) (lift (S O) O x7) x6))) \to P)))) (\lambda (H40: (eq T v4
1980 x)).(eq_ind T x (\lambda (_: T).((eq T t4 (THead (Bind x3) x4 x5)) \to ((eq T
1981 (THead (Flat Appl) v5 t5) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O)
1982 O x7) x6))) \to P))) (\lambda (H41: (eq T t4 (THead (Bind x3) x4
1983 x5))).(eq_ind T (THead (Bind x3) x4 x5) (\lambda (_: T).((eq T (THead (Flat
1984 Appl) v5 t5) (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)))
1985 \to P)) (\lambda (H42: (eq T (THead (Flat Appl) v5 t5) (THead (Bind x3) x8
1986 (THead (Flat Appl) (lift (S O) O x7) x6)))).(let H43 \def (eq_ind T (THead
1987 (Flat Appl) v5 t5) (\lambda (e: T).(match e with [(TSort _) \Rightarrow False
1988 | (TLRef _) \Rightarrow False | (THead k0 _ _) \Rightarrow (match k0 with
1989 [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind
1990 x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6)) H42) in (False_ind P H43)))
1991 t4 (sym_eq T t4 (THead (Bind x3) x4 x5) H41))) v4 (sym_eq T v4 x H40))) k
1992 (sym_eq K k (Flat Appl) H39))) H38)) H37)) H36)))]) in (H35 (refl_equal T
1993 (THead (Flat Appl) x (THead (Bind x3) x4 x5))) (refl_equal T (THead (Bind x3)
1994 x8 (THead (Flat Appl) (lift (S O) O x7) x6)))))))) (THead (Flat Appl) x1
1995 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O x7) x6))) (pr3_pr2 c
1996 (THead (Flat Appl) t0 (THead (Bind x3) x8 (THead (Flat Appl) (lift (S O) O
1997 x7) x6))) (THead (Flat Appl) x1 (THead (Bind x3) x8 (THead (Flat Appl) (lift
1998 (S O) O x7) x6))) (pr2_head_1 c t0 x1 H17 (Flat Appl) (THead (Bind x3) x8
1999 (THead (Flat Appl) (lift (S O) O x7) x6)))))))))) x2 H24)))))))))))))) H21))
2000 H20)) t3 H16))))))) H15)) (\lambda (H15: (ex4_4 T T T T (\lambda (y1:
2001 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Appl)
2002 x x0) (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda
2003 (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind Abbr) u2 t4)))))) (\lambda (_:
2004 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c t0 u2)))))
2005 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t4: T).(\forall
2006 (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t4))))))))).(ex4_4_ind T
2007 T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T
2008 (THead (Flat Appl) x x0) (THead (Bind Abst) y1 z1)))))) (\lambda (_:
2009 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t4: T).(eq T t3 (THead (Bind
2010 Abbr) u2 t4)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
2011 (_: T).(pr2 c t0 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
2012 T).(\lambda (t4: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
2013 z1 t4))))))) (sn3 c t3) (\lambda (x1: T).(\lambda (x2: T).(\lambda (x3:
2014 T).(\lambda (x4: T).(\lambda (H16: (eq T (THead (Flat Appl) x x0) (THead
2015 (Bind Abst) x1 x2))).(\lambda (H17: (eq T t3 (THead (Bind Abbr) x3
2016 x4))).(\lambda (_: (pr2 c t0 x3)).(\lambda (_: ((\forall (b: B).(\forall (u:
2017 T).(pr2 (CHead c (Bind b) u) x2 x4))))).(let H20 \def (eq_ind T t3 (\lambda
2018 (t: T).((eq T (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t) \to (\forall
2019 (P: Prop).P))) H12 (THead (Bind Abbr) x3 x4) H17) in (eq_ind_r T (THead (Bind
2020 Abbr) x3 x4) (\lambda (t: T).(sn3 c t)) (let H21 \def (eq_ind T (THead (Flat
2021 Appl) x x0) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False |
2022 (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind
2023 _) \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abst) x1
2024 x2) H16) in (False_ind (sn3 c (THead (Bind Abbr) x3 x4)) H21)) t3
2025 H17)))))))))) H15)) (\lambda (H15: (ex6_6 B T T T T T (\lambda (b:
2026 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
2027 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
2028 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat
2029 Appl) x x0) (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
2030 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
2031 t3 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
2032 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
2033 T).(\lambda (_: T).(pr2 c t0 u2))))))) (\lambda (_: B).(\lambda (y1:
2034 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
2035 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
2036 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1
2037 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda
2038 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b
2039 Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
2040 T).(\lambda (_: T).(\lambda (_: T).(eq T (THead (Flat Appl) x x0) (THead
2041 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
2042 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t3 (THead (Bind
2043 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
2044 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
2045 (_: T).(pr2 c t0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
2046 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
2047 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
2048 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))) (sn3 c t3)
2049 (\lambda (x1: B).(\lambda (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda
2050 (x5: T).(\lambda (x6: T).(\lambda (_: (not (eq B x1 Abst))).(\lambda (H17:
2051 (eq T (THead (Flat Appl) x x0) (THead (Bind x1) x2 x3))).(\lambda (H18: (eq T
2052 t3 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4)))).(\lambda
2053 (_: (pr2 c t0 x5)).(\lambda (_: (pr2 c x2 x6)).(\lambda (_: (pr2 (CHead c
2054 (Bind x1) x6) x3 x4)).(let H22 \def (eq_ind T t3 (\lambda (t: T).((eq T
2055 (THead (Flat Appl) t0 (THead (Flat Appl) x x0)) t) \to (\forall (P:
2056 Prop).P))) H12 (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5) x4))
2057 H18) in (eq_ind_r T (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O) O x5)
2058 x4)) (\lambda (t: T).(sn3 c t)) (let H23 \def (eq_ind T (THead (Flat Appl) x
2059 x0) (\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _)
2060 \Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _)
2061 \Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind x1) x2 x3)
2062 H17) in (False_ind (sn3 c (THead (Bind x1) x6 (THead (Flat Appl) (lift (S O)
2063 O x5) x4))) H23)) t3 H18)))))))))))))) H15)) H14)))))) t2 H3))))))))) v2
2064 H4))))))))) y H0))))) H))))).
2066 theorem sn3_appl_beta:
2067 \forall (c: C).(\forall (u: T).(\forall (v: T).(\forall (t: T).((sn3 c
2068 (THead (Flat Appl) u (THead (Bind Abbr) v t))) \to (\forall (w: T).((sn3 c w)
2069 \to (sn3 c (THead (Flat Appl) u (THead (Flat Appl) v (THead (Bind Abst) w
2072 \lambda (c: C).(\lambda (u: T).(\lambda (v: T).(\lambda (t: T).(\lambda (H:
2073 (sn3 c (THead (Flat Appl) u (THead (Bind Abbr) v t)))).(\lambda (w:
2074 T).(\lambda (H0: (sn3 c w)).(let H_x \def (sn3_gen_flat Appl c u (THead (Bind
2075 Abbr) v t) H) in (let H1 \def H_x in (land_ind (sn3 c u) (sn3 c (THead (Bind
2076 Abbr) v t)) (sn3 c (THead (Flat Appl) u (THead (Flat Appl) v (THead (Bind
2077 Abst) w t)))) (\lambda (H2: (sn3 c u)).(\lambda (H3: (sn3 c (THead (Bind
2078 Abbr) v t))).(sn3_appl_appl v (THead (Bind Abst) w t) c (sn3_beta c v t H3 w
2079 H0) u H2 (\lambda (u2: T).(\lambda (H4: (pr3 c (THead (Flat Appl) v (THead
2080 (Bind Abst) w t)) u2)).(\lambda (H5: (((iso (THead (Flat Appl) v (THead (Bind
2081 Abst) w t)) u2) \to (\forall (P: Prop).P)))).(sn3_pr3_trans c (THead (Flat
2082 Appl) u (THead (Bind Abbr) v t)) H (THead (Flat Appl) u u2) (pr3_thin_dx c
2083 (THead (Bind Abbr) v t) u2 (pr3_iso_beta v w t c u2 H4 H5) u Appl))))))))
2086 theorem sn3_appl_appls:
2087 \forall (v1: T).(\forall (t1: T).(\forall (vs: TList).(let u1 \def (THeads
2088 (Flat Appl) (TCons v1 vs) t1) in (\forall (c: C).((sn3 c u1) \to (\forall
2089 (v2: T).((sn3 c v2) \to (((\forall (u2: T).((pr3 c u1 u2) \to ((((iso u1 u2)
2090 \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat Appl) v2 u2)))))) \to
2091 (sn3 c (THead (Flat Appl) v2 u1))))))))))
2093 \lambda (v1: T).(\lambda (t1: T).(\lambda (vs: TList).(let u1 \def (THeads
2094 (Flat Appl) (TCons v1 vs) t1) in (\lambda (c: C).(\lambda (H: (sn3 c (THead
2095 (Flat Appl) v1 (THeads (Flat Appl) vs t1)))).(\lambda (v2: T).(\lambda (H0:
2096 (sn3 c v2)).(\lambda (H1: ((\forall (u2: T).((pr3 c (THead (Flat Appl) v1
2097 (THeads (Flat Appl) vs t1)) u2) \to ((((iso (THead (Flat Appl) v1 (THeads
2098 (Flat Appl) vs t1)) u2) \to (\forall (P: Prop).P))) \to (sn3 c (THead (Flat
2099 Appl) v2 u2))))))).(sn3_appl_appl v1 (THeads (Flat Appl) vs t1) c H v2 H0
2102 lemma sn3_appls_lref:
2103 \forall (c: C).(\forall (i: nat).((nf2 c (TLRef i)) \to (\forall (us:
2104 TList).((sns3 c us) \to (sn3 c (THeads (Flat Appl) us (TLRef i)))))))
2106 \lambda (c: C).(\lambda (i: nat).(\lambda (H: (nf2 c (TLRef i))).(\lambda
2107 (us: TList).(TList_ind (\lambda (t: TList).((sns3 c t) \to (sn3 c (THeads
2108 (Flat Appl) t (TLRef i))))) (\lambda (_: True).(sn3_nf2 c (TLRef i) H))
2109 (\lambda (t: T).(\lambda (t0: TList).(TList_ind (\lambda (t1: TList).((((sns3
2110 c t1) \to (sn3 c (THeads (Flat Appl) t1 (TLRef i))))) \to ((land (sn3 c t)
2111 (sns3 c t1)) \to (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t1 (TLRef
2112 i))))))) (\lambda (_: (((sns3 c TNil) \to (sn3 c (THeads (Flat Appl) TNil
2113 (TLRef i)))))).(\lambda (H1: (land (sn3 c t) (sns3 c TNil))).(let H2 \def H1
2114 in (land_ind (sn3 c t) True (sn3 c (THead (Flat Appl) t (THeads (Flat Appl)
2115 TNil (TLRef i)))) (\lambda (H3: (sn3 c t)).(\lambda (_: True).(sn3_appl_lref
2116 c i H t H3))) H2)))) (\lambda (t1: T).(\lambda (t2: TList).(\lambda (_:
2117 (((((sns3 c t2) \to (sn3 c (THeads (Flat Appl) t2 (TLRef i))))) \to ((land
2118 (sn3 c t) (sns3 c t2)) \to (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t2
2119 (TLRef i)))))))).(\lambda (H1: (((sns3 c (TCons t1 t2)) \to (sn3 c (THeads
2120 (Flat Appl) (TCons t1 t2) (TLRef i)))))).(\lambda (H2: (land (sn3 c t) (sns3
2121 c (TCons t1 t2)))).(let H3 \def H2 in (land_ind (sn3 c t) (land (sn3 c t1)
2122 (sns3 c t2)) (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2)
2123 (TLRef i)))) (\lambda (H4: (sn3 c t)).(\lambda (H5: (land (sn3 c t1) (sns3 c
2124 t2))).(land_ind (sn3 c t1) (sns3 c t2) (sn3 c (THead (Flat Appl) t (THeads
2125 (Flat Appl) (TCons t1 t2) (TLRef i)))) (\lambda (H6: (sn3 c t1)).(\lambda
2126 (H7: (sns3 c t2)).(sn3_appl_appls t1 (TLRef i) t2 c (H1 (conj (sn3 c t1)
2127 (sns3 c t2) H6 H7)) t H4 (\lambda (u2: T).(\lambda (H8: (pr3 c (THeads (Flat
2128 Appl) (TCons t1 t2) (TLRef i)) u2)).(\lambda (H9: (((iso (THeads (Flat Appl)
2129 (TCons t1 t2) (TLRef i)) u2) \to (\forall (P: Prop).P)))).(H9
2130 (nf2_iso_appls_lref c i H (TCons t1 t2) u2 H8) (sn3 c (THead (Flat Appl) t
2131 u2))))))))) H5))) H3))))))) t0))) us)))).
2133 theorem sn3_appls_cast:
2134 \forall (c: C).(\forall (vs: TList).(\forall (u: T).((sn3 c (THeads (Flat
2135 Appl) vs u)) \to (\forall (t: T).((sn3 c (THeads (Flat Appl) vs t)) \to (sn3
2136 c (THeads (Flat Appl) vs (THead (Flat Cast) u t))))))))
2138 \lambda (c: C).(\lambda (vs: TList).(TList_ind (\lambda (t: TList).(\forall
2139 (u: T).((sn3 c (THeads (Flat Appl) t u)) \to (\forall (t0: T).((sn3 c (THeads
2140 (Flat Appl) t t0)) \to (sn3 c (THeads (Flat Appl) t (THead (Flat Cast) u
2141 t0)))))))) (\lambda (u: T).(\lambda (H: (sn3 c u)).(\lambda (t: T).(\lambda
2142 (H0: (sn3 c t)).(sn3_cast c u H t H0))))) (\lambda (t: T).(\lambda (t0:
2143 TList).(TList_ind (\lambda (t1: TList).(((\forall (u: T).((sn3 c (THeads
2144 (Flat Appl) t1 u)) \to (\forall (t2: T).((sn3 c (THeads (Flat Appl) t1 t2))
2145 \to (sn3 c (THeads (Flat Appl) t1 (THead (Flat Cast) u t2)))))))) \to
2146 (\forall (u: T).((sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t1 u))) \to
2147 (\forall (t2: T).((sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t1 t2)))
2148 \to (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t1 (THead (Flat Cast) u
2149 t2)))))))))) (\lambda (_: ((\forall (u: T).((sn3 c (THeads (Flat Appl) TNil
2150 u)) \to (\forall (t1: T).((sn3 c (THeads (Flat Appl) TNil t1)) \to (sn3 c
2151 (THeads (Flat Appl) TNil (THead (Flat Cast) u t1))))))))).(\lambda (u:
2152 T).(\lambda (H0: (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) TNil
2153 u)))).(\lambda (t1: T).(\lambda (H1: (sn3 c (THead (Flat Appl) t (THeads
2154 (Flat Appl) TNil t1)))).(sn3_appl_cast c t u H0 t1 H1)))))) (\lambda (t1:
2155 T).(\lambda (t2: TList).(\lambda (_: ((((\forall (u: T).((sn3 c (THeads (Flat
2156 Appl) t2 u)) \to (\forall (t3: T).((sn3 c (THeads (Flat Appl) t2 t3)) \to
2157 (sn3 c (THeads (Flat Appl) t2 (THead (Flat Cast) u t3)))))))) \to (\forall
2158 (u: T).((sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t2 u))) \to (\forall
2159 (t3: T).((sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t2 t3))) \to (sn3 c
2160 (THead (Flat Appl) t (THeads (Flat Appl) t2 (THead (Flat Cast) u
2161 t3))))))))))).(\lambda (H0: ((\forall (u: T).((sn3 c (THeads (Flat Appl)
2162 (TCons t1 t2) u)) \to (\forall (t3: T).((sn3 c (THeads (Flat Appl) (TCons t1
2163 t2) t3)) \to (sn3 c (THeads (Flat Appl) (TCons t1 t2) (THead (Flat Cast) u
2164 t3))))))))).(\lambda (u: T).(\lambda (H1: (sn3 c (THead (Flat Appl) t (THeads
2165 (Flat Appl) (TCons t1 t2) u)))).(\lambda (t3: T).(\lambda (H2: (sn3 c (THead
2166 (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2) t3)))).(let H_x \def
2167 (sn3_gen_flat Appl c t (THeads (Flat Appl) (TCons t1 t2) t3) H2) in (let H3
2168 \def H_x in (land_ind (sn3 c t) (sn3 c (THead (Flat Appl) t1 (THeads (Flat
2169 Appl) t2 t3))) (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1 t2)
2170 (THead (Flat Cast) u t3)))) (\lambda (_: (sn3 c t)).(\lambda (H5: (sn3 c
2171 (THead (Flat Appl) t1 (THeads (Flat Appl) t2 t3)))).(let H6 \def H5 in (let
2172 H_x0 \def (sn3_gen_flat Appl c t (THeads (Flat Appl) (TCons t1 t2) u) H1) in
2173 (let H7 \def H_x0 in (land_ind (sn3 c t) (sn3 c (THead (Flat Appl) t1 (THeads
2174 (Flat Appl) t2 u))) (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) (TCons t1
2175 t2) (THead (Flat Cast) u t3)))) (\lambda (H8: (sn3 c t)).(\lambda (H9: (sn3 c
2176 (THead (Flat Appl) t1 (THeads (Flat Appl) t2 u)))).(let H10 \def H9 in
2177 (sn3_appl_appls t1 (THead (Flat Cast) u t3) t2 c (H0 u H10 t3 H6) t H8
2178 (\lambda (u2: T).(\lambda (H11: (pr3 c (THeads (Flat Appl) (TCons t1 t2)
2179 (THead (Flat Cast) u t3)) u2)).(\lambda (H12: (((iso (THeads (Flat Appl)
2180 (TCons t1 t2) (THead (Flat Cast) u t3)) u2) \to (\forall (P:
2181 Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) t (THeads (Flat Appl) (TCons
2182 t1 t2) t3)) H2 (THead (Flat Appl) t u2) (pr3_thin_dx c (THeads (Flat Appl)
2183 (TCons t1 t2) t3) u2 (pr3_iso_appls_cast c u t3 (TCons t1 t2) u2 H11 H12) t
2184 Appl))))))))) H7)))))) H3))))))))))) t0))) vs)).
2186 theorem sn3_appls_bind:
2187 \forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (u:
2188 T).((sn3 c u) \to (\forall (vs: TList).(\forall (t: T).((sn3 (CHead c (Bind
2189 b) u) (THeads (Flat Appl) (lifts (S O) O vs) t)) \to (sn3 c (THeads (Flat
2190 Appl) vs (THead (Bind b) u t))))))))))
2192 \lambda (b: B).(\lambda (H: (not (eq B b Abst))).(\lambda (c: C).(\lambda
2193 (u: T).(\lambda (H0: (sn3 c u)).(\lambda (vs: TList).(TList_ind (\lambda (t:
2194 TList).(\forall (t0: T).((sn3 (CHead c (Bind b) u) (THeads (Flat Appl) (lifts
2195 (S O) O t) t0)) \to (sn3 c (THeads (Flat Appl) t (THead (Bind b) u t0))))))
2196 (\lambda (t: T).(\lambda (H1: (sn3 (CHead c (Bind b) u) t)).(sn3_bind b c u
2197 H0 t H1))) (\lambda (v: T).(\lambda (vs0: TList).(TList_ind (\lambda (t:
2198 TList).(((\forall (t0: T).((sn3 (CHead c (Bind b) u) (THeads (Flat Appl)
2199 (lifts (S O) O t) t0)) \to (sn3 c (THeads (Flat Appl) t (THead (Bind b) u
2200 t0)))))) \to (\forall (t0: T).((sn3 (CHead c (Bind b) u) (THead (Flat Appl)
2201 (lift (S O) O v) (THeads (Flat Appl) (lifts (S O) O t) t0))) \to (sn3 c
2202 (THead (Flat Appl) v (THeads (Flat Appl) t (THead (Bind b) u t0))))))))
2203 (\lambda (_: ((\forall (t: T).((sn3 (CHead c (Bind b) u) (THeads (Flat Appl)
2204 (lifts (S O) O TNil) t)) \to (sn3 c (THeads (Flat Appl) TNil (THead (Bind b)
2205 u t))))))).(\lambda (t: T).(\lambda (H2: (sn3 (CHead c (Bind b) u) (THead
2206 (Flat Appl) (lift (S O) O v) (THeads (Flat Appl) (lifts (S O) O TNil)
2207 t)))).(sn3_appl_bind b H c u H0 t v H2)))) (\lambda (t: T).(\lambda (t0:
2208 TList).(\lambda (_: ((((\forall (t1: T).((sn3 (CHead c (Bind b) u) (THeads
2209 (Flat Appl) (lifts (S O) O t0) t1)) \to (sn3 c (THeads (Flat Appl) t0 (THead
2210 (Bind b) u t1)))))) \to (\forall (t1: T).((sn3 (CHead c (Bind b) u) (THead
2211 (Flat Appl) (lift (S O) O v) (THeads (Flat Appl) (lifts (S O) O t0) t1))) \to
2212 (sn3 c (THead (Flat Appl) v (THeads (Flat Appl) t0 (THead (Bind b) u
2213 t1))))))))).(\lambda (H2: ((\forall (t1: T).((sn3 (CHead c (Bind b) u)
2214 (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1)) \to (sn3 c (THeads
2215 (Flat Appl) (TCons t t0) (THead (Bind b) u t1))))))).(\lambda (t1:
2216 T).(\lambda (H3: (sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O
2217 v) (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1)))).(let H_x \def
2218 (sn3_gen_flat Appl (CHead c (Bind b) u) (lift (S O) O v) (THeads (Flat Appl)
2219 (lifts (S O) O (TCons t t0)) t1) H3) in (let H4 \def H_x in (land_ind (sn3
2220 (CHead c (Bind b) u) (lift (S O) O v)) (sn3 (CHead c (Bind b) u) (THead (Flat
2221 Appl) (lift (S O) O t) (THeads (Flat Appl) (lifts (S O) O t0) t1))) (sn3 c
2222 (THead (Flat Appl) v (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u
2223 t1)))) (\lambda (H5: (sn3 (CHead c (Bind b) u) (lift (S O) O v))).(\lambda
2224 (H6: (sn3 (CHead c (Bind b) u) (THead (Flat Appl) (lift (S O) O t) (THeads
2225 (Flat Appl) (lifts (S O) O t0) t1)))).(let H_y \def (sn3_gen_lift (CHead c
2226 (Bind b) u) v (S O) O H5 c) in (sn3_appl_appls t (THead (Bind b) u t1) t0 c
2227 (H2 t1 H6) v (H_y (drop_drop (Bind b) O c c (drop_refl c) u)) (\lambda (u2:
2228 T).(\lambda (H7: (pr3 c (THeads (Flat Appl) (TCons t t0) (THead (Bind b) u
2229 t1)) u2)).(\lambda (H8: (((iso (THeads (Flat Appl) (TCons t t0) (THead (Bind
2230 b) u t1)) u2) \to (\forall (P: Prop).P)))).(let H9 \def (pr3_iso_appls_bind b
2231 H (TCons t t0) u t1 c u2 H7 H8) in (sn3_pr3_trans c (THead (Flat Appl) v
2232 (THead (Bind b) u (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1)))
2233 (sn3_appl_bind b H c u H0 (THeads (Flat Appl) (lifts (S O) O (TCons t t0))
2234 t1) v H3) (THead (Flat Appl) v u2) (pr3_flat c v v (pr3_refl c v) (THead
2235 (Bind b) u (THeads (Flat Appl) (lifts (S O) O (TCons t t0)) t1)) u2 H9
2236 Appl)))))))))) H4))))))))) vs0))) vs)))))).
2238 theorem sn3_appls_beta:
2239 \forall (c: C).(\forall (v: T).(\forall (t: T).(\forall (us: TList).((sn3 c
2240 (THeads (Flat Appl) us (THead (Bind Abbr) v t))) \to (\forall (w: T).((sn3 c
2241 w) \to (sn3 c (THeads (Flat Appl) us (THead (Flat Appl) v (THead (Bind Abst)
2244 \lambda (c: C).(\lambda (v: T).(\lambda (t: T).(\lambda (us:
2245 TList).(TList_ind (\lambda (t0: TList).((sn3 c (THeads (Flat Appl) t0 (THead
2246 (Bind Abbr) v t))) \to (\forall (w: T).((sn3 c w) \to (sn3 c (THeads (Flat
2247 Appl) t0 (THead (Flat Appl) v (THead (Bind Abst) w t)))))))) (\lambda (H:
2248 (sn3 c (THead (Bind Abbr) v t))).(\lambda (w: T).(\lambda (H0: (sn3 c
2249 w)).(sn3_beta c v t H w H0)))) (\lambda (u: T).(\lambda (us0:
2250 TList).(TList_ind (\lambda (t0: TList).((((sn3 c (THeads (Flat Appl) t0
2251 (THead (Bind Abbr) v t))) \to (\forall (w: T).((sn3 c w) \to (sn3 c (THeads
2252 (Flat Appl) t0 (THead (Flat Appl) v (THead (Bind Abst) w t)))))))) \to ((sn3
2253 c (THead (Flat Appl) u (THeads (Flat Appl) t0 (THead (Bind Abbr) v t)))) \to
2254 (\forall (w: T).((sn3 c w) \to (sn3 c (THead (Flat Appl) u (THeads (Flat
2255 Appl) t0 (THead (Flat Appl) v (THead (Bind Abst) w t)))))))))) (\lambda (_:
2256 (((sn3 c (THeads (Flat Appl) TNil (THead (Bind Abbr) v t))) \to (\forall (w:
2257 T).((sn3 c w) \to (sn3 c (THeads (Flat Appl) TNil (THead (Flat Appl) v (THead
2258 (Bind Abst) w t))))))))).(\lambda (H0: (sn3 c (THead (Flat Appl) u (THeads
2259 (Flat Appl) TNil (THead (Bind Abbr) v t))))).(\lambda (w: T).(\lambda (H1:
2260 (sn3 c w)).(sn3_appl_beta c u v t H0 w H1))))) (\lambda (t0: T).(\lambda (t1:
2261 TList).(\lambda (_: (((((sn3 c (THeads (Flat Appl) t1 (THead (Bind Abbr) v
2262 t))) \to (\forall (w: T).((sn3 c w) \to (sn3 c (THeads (Flat Appl) t1 (THead
2263 (Flat Appl) v (THead (Bind Abst) w t)))))))) \to ((sn3 c (THead (Flat Appl) u
2264 (THeads (Flat Appl) t1 (THead (Bind Abbr) v t)))) \to (\forall (w: T).((sn3 c
2265 w) \to (sn3 c (THead (Flat Appl) u (THeads (Flat Appl) t1 (THead (Flat Appl)
2266 v (THead (Bind Abst) w t))))))))))).(\lambda (H0: (((sn3 c (THeads (Flat
2267 Appl) (TCons t0 t1) (THead (Bind Abbr) v t))) \to (\forall (w: T).((sn3 c w)
2268 \to (sn3 c (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Appl) v (THead
2269 (Bind Abst) w t))))))))).(\lambda (H1: (sn3 c (THead (Flat Appl) u (THeads
2270 (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t))))).(\lambda (w:
2271 T).(\lambda (H2: (sn3 c w)).(let H_x \def (sn3_gen_flat Appl c u (THeads
2272 (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v t)) H1) in (let H3 \def H_x in
2273 (land_ind (sn3 c u) (sn3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1
2274 (THead (Bind Abbr) v t)))) (sn3 c (THead (Flat Appl) u (THeads (Flat Appl)
2275 (TCons t0 t1) (THead (Flat Appl) v (THead (Bind Abst) w t))))) (\lambda (H4:
2276 (sn3 c u)).(\lambda (H5: (sn3 c (THead (Flat Appl) t0 (THeads (Flat Appl) t1
2277 (THead (Bind Abbr) v t))))).(sn3_appl_appls t0 (THead (Flat Appl) v (THead
2278 (Bind Abst) w t)) t1 c (H0 H5 w H2) u H4 (\lambda (u2: T).(\lambda (H6: (pr3
2279 c (THeads (Flat Appl) (TCons t0 t1) (THead (Flat Appl) v (THead (Bind Abst) w
2280 t))) u2)).(\lambda (H7: (((iso (THeads (Flat Appl) (TCons t0 t1) (THead (Flat
2281 Appl) v (THead (Bind Abst) w t))) u2) \to (\forall (P: Prop).P)))).(let H8
2282 \def (pr3_iso_appls_beta (TCons t0 t1) v w t c u2 H6 H7) in (sn3_pr3_trans c
2283 (THead (Flat Appl) u (THeads (Flat Appl) (TCons t0 t1) (THead (Bind Abbr) v
2284 t))) H1 (THead (Flat Appl) u u2) (pr3_thin_dx c (THeads (Flat Appl) (TCons t0
2285 t1) (THead (Bind Abbr) v t)) u2 H8 u Appl))))))))) H3)))))))))) us0))) us)))).
2288 \forall (d: C).(\forall (t: T).((sn3 d t) \to (\forall (c: C).(\forall (h:
2289 nat).(\forall (i: nat).((drop h i c d) \to (sn3 c (lift h i t))))))))
2291 \lambda (d: C).(\lambda (t: T).(\lambda (H: (sn3 d t)).(sn3_ind d (\lambda
2292 (t0: T).(\forall (c: C).(\forall (h: nat).(\forall (i: nat).((drop h i c d)
2293 \to (sn3 c (lift h i t0))))))) (\lambda (t1: T).(\lambda (_: ((\forall (t2:
2294 T).((((eq T t1 t2) \to (\forall (P: Prop).P))) \to ((pr3 d t1 t2) \to (sn3 d
2295 t2)))))).(\lambda (H1: ((\forall (t2: T).((((eq T t1 t2) \to (\forall (P:
2296 Prop).P))) \to ((pr3 d t1 t2) \to (\forall (c: C).(\forall (h: nat).(\forall
2297 (i: nat).((drop h i c d) \to (sn3 c (lift h i t2))))))))))).(\lambda (c:
2298 C).(\lambda (h: nat).(\lambda (i: nat).(\lambda (H2: (drop h i c
2299 d)).(sn3_pr2_intro c (lift h i t1) (\lambda (t2: T).(\lambda (H3: (((eq T
2300 (lift h i t1) t2) \to (\forall (P: Prop).P)))).(\lambda (H4: (pr2 c (lift h i
2301 t1) t2)).(let H5 \def (pr2_gen_lift c t1 t2 h i H4 d H2) in (ex2_ind T
2302 (\lambda (t3: T).(eq T t2 (lift h i t3))) (\lambda (t3: T).(pr2 d t1 t3))
2303 (sn3 c t2) (\lambda (x: T).(\lambda (H6: (eq T t2 (lift h i x))).(\lambda
2304 (H7: (pr2 d t1 x)).(let H8 \def (eq_ind T t2 (\lambda (t0: T).((eq T (lift h
2305 i t1) t0) \to (\forall (P: Prop).P))) H3 (lift h i x) H6) in (eq_ind_r T
2306 (lift h i x) (\lambda (t0: T).(sn3 c t0)) (H1 x (\lambda (H9: (eq T t1
2307 x)).(\lambda (P: Prop).(let H10 \def (eq_ind_r T x (\lambda (t0: T).((eq T
2308 (lift h i t1) (lift h i t0)) \to (\forall (P0: Prop).P0))) H8 t1 H9) in (let
2309 H11 \def (eq_ind_r T x (\lambda (t0: T).(pr2 d t1 t0)) H7 t1 H9) in (H10
2310 (refl_equal T (lift h i t1)) P))))) (pr3_pr2 d t1 x H7) c h i H2) t2 H6)))))
2311 H5))))))))))))) t H))).
2314 \forall (c: C).(\forall (d: C).(\forall (v: T).(\forall (i: nat).((getl i c
2315 (CHead d (Bind Abbr) v)) \to ((sn3 d v) \to (sn3 c (TLRef i)))))))
2317 \lambda (c: C).(\lambda (d: C).(\lambda (v: T).(\lambda (i: nat).(\lambda
2318 (H: (getl i c (CHead d (Bind Abbr) v))).(\lambda (H0: (sn3 d
2319 v)).(sn3_pr2_intro c (TLRef i) (\lambda (t2: T).(\lambda (H1: (((eq T (TLRef
2320 i) t2) \to (\forall (P: Prop).P)))).(\lambda (H2: (pr2 c (TLRef i) t2)).(let
2321 H3 \def (pr2_gen_lref c t2 i H2) in (or_ind (eq T t2 (TLRef i)) (ex2_2 C T
2322 (\lambda (d0: C).(\lambda (u: T).(getl i c (CHead d0 (Bind Abbr) u))))
2323 (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift (S i) O u))))) (sn3 c t2)
2324 (\lambda (H4: (eq T t2 (TLRef i))).(let H5 \def (eq_ind T t2 (\lambda (t:
2325 T).((eq T (TLRef i) t) \to (\forall (P: Prop).P))) H1 (TLRef i) H4) in
2326 (eq_ind_r T (TLRef i) (\lambda (t: T).(sn3 c t)) (H5 (refl_equal T (TLRef i))
2327 (sn3 c (TLRef i))) t2 H4))) (\lambda (H4: (ex2_2 C T (\lambda (d0:
2328 C).(\lambda (u: T).(getl i c (CHead d0 (Bind Abbr) u)))) (\lambda (_:
2329 C).(\lambda (u: T).(eq T t2 (lift (S i) O u)))))).(ex2_2_ind C T (\lambda
2330 (d0: C).(\lambda (u: T).(getl i c (CHead d0 (Bind Abbr) u)))) (\lambda (_:
2331 C).(\lambda (u: T).(eq T t2 (lift (S i) O u)))) (sn3 c t2) (\lambda (x0:
2332 C).(\lambda (x1: T).(\lambda (H5: (getl i c (CHead x0 (Bind Abbr)
2333 x1))).(\lambda (H6: (eq T t2 (lift (S i) O x1))).(let H7 \def (eq_ind T t2
2334 (\lambda (t: T).((eq T (TLRef i) t) \to (\forall (P: Prop).P))) H1 (lift (S
2335 i) O x1) H6) in (eq_ind_r T (lift (S i) O x1) (\lambda (t: T).(sn3 c t)) (let
2336 H8 \def (eq_ind C (CHead d (Bind Abbr) v) (\lambda (c0: C).(getl i c c0)) H
2337 (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead d (Bind Abbr) v) i H (CHead x0
2338 (Bind Abbr) x1) H5)) in (let H9 \def (f_equal C C (\lambda (e: C).(match e
2339 with [(CSort _) \Rightarrow d | (CHead c0 _ _) \Rightarrow c0])) (CHead d
2340 (Bind Abbr) v) (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead d (Bind Abbr) v)
2341 i H (CHead x0 (Bind Abbr) x1) H5)) in ((let H10 \def (f_equal C T (\lambda
2342 (e: C).(match e with [(CSort _) \Rightarrow v | (CHead _ _ t) \Rightarrow
2343 t])) (CHead d (Bind Abbr) v) (CHead x0 (Bind Abbr) x1) (getl_mono c (CHead d
2344 (Bind Abbr) v) i H (CHead x0 (Bind Abbr) x1) H5)) in (\lambda (H11: (eq C d
2345 x0)).(let H12 \def (eq_ind_r T x1 (\lambda (t: T).(getl i c (CHead x0 (Bind
2346 Abbr) t))) H8 v H10) in (eq_ind T v (\lambda (t: T).(sn3 c (lift (S i) O t)))
2347 (let H13 \def (eq_ind_r C x0 (\lambda (c0: C).(getl i c (CHead c0 (Bind Abbr)
2348 v))) H12 d H11) in (sn3_lift d v H0 c (S i) O (getl_drop Abbr c d v i H13)))
2349 x1 H10)))) H9))) t2 H6)))))) H4)) H3))))))))))).
2351 lemma sn3_appls_abbr:
2352 \forall (c: C).(\forall (d: C).(\forall (w: T).(\forall (i: nat).((getl i c
2353 (CHead d (Bind Abbr) w)) \to (\forall (vs: TList).((sn3 c (THeads (Flat Appl)
2354 vs (lift (S i) O w))) \to (sn3 c (THeads (Flat Appl) vs (TLRef i)))))))))
2356 \lambda (c: C).(\lambda (d: C).(\lambda (w: T).(\lambda (i: nat).(\lambda
2357 (H: (getl i c (CHead d (Bind Abbr) w))).(\lambda (vs: TList).(TList_ind
2358 (\lambda (t: TList).((sn3 c (THeads (Flat Appl) t (lift (S i) O w))) \to (sn3
2359 c (THeads (Flat Appl) t (TLRef i))))) (\lambda (H0: (sn3 c (lift (S i) O
2360 w))).(let H_y \def (sn3_gen_lift c w (S i) O H0 d (getl_drop Abbr c d w i H))
2361 in (sn3_abbr c d w i H H_y))) (\lambda (v: T).(\lambda (vs0:
2362 TList).(TList_ind (\lambda (t: TList).((((sn3 c (THeads (Flat Appl) t (lift
2363 (S i) O w))) \to (sn3 c (THeads (Flat Appl) t (TLRef i))))) \to ((sn3 c
2364 (THead (Flat Appl) v (THeads (Flat Appl) t (lift (S i) O w)))) \to (sn3 c
2365 (THead (Flat Appl) v (THeads (Flat Appl) t (TLRef i))))))) (\lambda (_:
2366 (((sn3 c (THeads (Flat Appl) TNil (lift (S i) O w))) \to (sn3 c (THeads (Flat
2367 Appl) TNil (TLRef i)))))).(\lambda (H1: (sn3 c (THead (Flat Appl) v (THeads
2368 (Flat Appl) TNil (lift (S i) O w))))).(sn3_appl_abbr c d w i H v H1)))
2369 (\lambda (t: T).(\lambda (t0: TList).(\lambda (_: (((((sn3 c (THeads (Flat
2370 Appl) t0 (lift (S i) O w))) \to (sn3 c (THeads (Flat Appl) t0 (TLRef i)))))
2371 \to ((sn3 c (THead (Flat Appl) v (THeads (Flat Appl) t0 (lift (S i) O w))))
2372 \to (sn3 c (THead (Flat Appl) v (THeads (Flat Appl) t0 (TLRef
2373 i)))))))).(\lambda (H1: (((sn3 c (THeads (Flat Appl) (TCons t t0) (lift (S i)
2374 O w))) \to (sn3 c (THeads (Flat Appl) (TCons t t0) (TLRef i)))))).(\lambda
2375 (H2: (sn3 c (THead (Flat Appl) v (THeads (Flat Appl) (TCons t t0) (lift (S i)
2376 O w))))).(let H_x \def (sn3_gen_flat Appl c v (THeads (Flat Appl) (TCons t
2377 t0) (lift (S i) O w)) H2) in (let H3 \def H_x in (land_ind (sn3 c v) (sn3 c
2378 (THead (Flat Appl) t (THeads (Flat Appl) t0 (lift (S i) O w)))) (sn3 c (THead
2379 (Flat Appl) v (THeads (Flat Appl) (TCons t t0) (TLRef i)))) (\lambda (H4:
2380 (sn3 c v)).(\lambda (H5: (sn3 c (THead (Flat Appl) t (THeads (Flat Appl) t0
2381 (lift (S i) O w))))).(sn3_appl_appls t (TLRef i) t0 c (H1 H5) v H4 (\lambda
2382 (u2: T).(\lambda (H6: (pr3 c (THeads (Flat Appl) (TCons t t0) (TLRef i))
2383 u2)).(\lambda (H7: (((iso (THeads (Flat Appl) (TCons t t0) (TLRef i)) u2) \to
2384 (\forall (P: Prop).P)))).(sn3_pr3_trans c (THead (Flat Appl) v (THeads (Flat
2385 Appl) (TCons t t0) (lift (S i) O w))) H2 (THead (Flat Appl) v u2)
2386 (pr3_thin_dx c (THeads (Flat Appl) (TCons t t0) (lift (S i) O w)) u2
2387 (pr3_iso_appls_abbr c d w i H (TCons t t0) u2 H6 H7) v Appl))))))))
2388 H3)))))))) vs0))) vs)))))).
2391 \forall (c: C).(\forall (d: C).(\forall (h: nat).(\forall (i: nat).((drop h
2392 i c d) \to (\forall (ts: TList).((sns3 d ts) \to (sns3 c (lifts h i ts))))))))
2394 \lambda (c: C).(\lambda (d: C).(\lambda (h: nat).(\lambda (i: nat).(\lambda
2395 (H: (drop h i c d)).(\lambda (ts: TList).(TList_ind (\lambda (t:
2396 TList).((sns3 d t) \to (sns3 c (lifts h i t)))) (\lambda (H0: True).H0)
2397 (\lambda (t: T).(\lambda (t0: TList).(\lambda (H0: (((sns3 d t0) \to (sns3 c
2398 (lifts h i t0))))).(\lambda (H1: (land (sn3 d t) (sns3 d t0))).(let H2 \def
2399 H1 in (land_ind (sn3 d t) (sns3 d t0) (land (sn3 c (lift h i t)) (sns3 c
2400 (lifts h i t0))) (\lambda (H3: (sn3 d t)).(\lambda (H4: (sns3 d t0)).(conj
2401 (sn3 c (lift h i t)) (sns3 c (lifts h i t0)) (sn3_lift d t H3 c h i H) (H0
2402 H4)))) H2)))))) ts)))))).