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