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