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/pr2/fwd.ma".
22 \forall (c: C).(\forall (x: T).(\forall (n: nat).((pr3 c (TSort n) x) \to
25 \lambda (c: C).(\lambda (x: T).(\lambda (n: nat).(\lambda (H: (pr3 c (TSort
26 n) x)).(insert_eq T (TSort n) (\lambda (t: T).(pr3 c t x)) (\lambda (t:
27 T).(eq T x t)) (\lambda (y: T).(\lambda (H0: (pr3 c y x)).(pr3_ind c (\lambda
28 (t: T).(\lambda (t0: T).((eq T t (TSort n)) \to (eq T t0 t)))) (\lambda (t:
29 T).(\lambda (_: (eq T t (TSort n))).(refl_equal T t))) (\lambda (t2:
30 T).(\lambda (t1: T).(\lambda (H1: (pr2 c t1 t2)).(\lambda (t3: T).(\lambda
31 (_: (pr3 c t2 t3)).(\lambda (H3: (((eq T t2 (TSort n)) \to (eq T t3
32 t2)))).(\lambda (H4: (eq T t1 (TSort n))).(let H5 \def (eq_ind T t1 (\lambda
33 (t: T).(pr2 c t t2)) H1 (TSort n) H4) in (eq_ind_r T (TSort n) (\lambda (t:
34 T).(eq T t3 t)) (let H6 \def (eq_ind T t2 (\lambda (t: T).((eq T t (TSort n))
35 \to (eq T t3 t))) H3 (TSort n) (pr2_gen_sort c t2 n H5)) in (H6 (refl_equal T
36 (TSort n)))) t1 H4))))))))) y x H0))) H)))).
42 \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
43 (THead (Bind Abst) u1 t1) x) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
44 T).(eq T x (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3
45 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall (u:
46 T).(pr3 (CHead c (Bind b) u) t1 t2))))))))))
48 \lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda
49 (H: (pr3 c (THead (Bind Abst) u1 t1) x)).(insert_eq T (THead (Bind Abst) u1
50 t1) (\lambda (t: T).(pr3 c t x)) (\lambda (_: T).(ex3_2 T T (\lambda (u2:
51 T).(\lambda (t2: T).(eq T x (THead (Bind Abst) u2 t2)))) (\lambda (u2:
52 T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall
53 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t1 t2))))))) (\lambda (y:
54 T).(\lambda (H0: (pr3 c y x)).(unintro T t1 (\lambda (t: T).((eq T y (THead
55 (Bind Abst) u1 t)) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x
56 (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2)))
57 (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead
58 c (Bind b) u) t t2)))))))) (unintro T u1 (\lambda (t: T).(\forall (x0:
59 T).((eq T y (THead (Bind Abst) t x0)) \to (ex3_2 T T (\lambda (u2:
60 T).(\lambda (t2: T).(eq T x (THead (Bind Abst) u2 t2)))) (\lambda (u2:
61 T).(\lambda (_: T).(pr3 c t u2))) (\lambda (_: T).(\lambda (t2: T).(\forall
62 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x0 t2))))))))) (pr3_ind c
63 (\lambda (t: T).(\lambda (t0: T).(\forall (x0: T).(\forall (x1: T).((eq T t
64 (THead (Bind Abst) x0 x1)) \to (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
65 T).(eq T t0 (THead (Bind Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_:
66 T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall
67 (u: T).(pr3 (CHead c (Bind b) u) x1 t2))))))))))) (\lambda (t: T).(\lambda
68 (x0: T).(\lambda (x1: T).(\lambda (H1: (eq T t (THead (Bind Abst) x0
69 x1))).(ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T t (THead (Bind
70 Abst) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
71 T).(\lambda (t2: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
72 x1 t2))))) x0 x1 H1 (pr3_refl c x0) (\lambda (b: B).(\lambda (u: T).(pr3_refl
73 (CHead c (Bind b) u) x1)))))))) (\lambda (t2: T).(\lambda (t3: T).(\lambda
74 (H1: (pr2 c t3 t2)).(\lambda (t4: T).(\lambda (_: (pr3 c t2 t4)).(\lambda
75 (H3: ((\forall (x0: T).(\forall (x1: T).((eq T t2 (THead (Bind Abst) x0 x1))
76 \to (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Abst)
77 u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
78 T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
79 x1 t5))))))))))).(\lambda (x0: T).(\lambda (x1: T).(\lambda (H4: (eq T t3
80 (THead (Bind Abst) x0 x1))).(let H5 \def (eq_ind T t3 (\lambda (t: T).(pr2 c
81 t t2)) H1 (THead (Bind Abst) x0 x1) H4) in (let H6 \def (pr2_gen_abst c x0 x1
82 t2 H5) in (ex3_2_ind T T (\lambda (u2: T).(\lambda (t5: T).(eq T t2 (THead
83 (Bind Abst) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2)))
84 (\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead
85 c (Bind b) u) x1 t5))))) (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T
86 t4 (THead (Bind Abst) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0
87 u2))) (\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3
88 (CHead c (Bind b) u) x1 t5)))))) (\lambda (x2: T).(\lambda (x3: T).(\lambda
89 (H7: (eq T t2 (THead (Bind Abst) x2 x3))).(\lambda (H8: (pr2 c x0
90 x2)).(\lambda (H9: ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
91 x1 x3))))).(let H10 \def (eq_ind T t2 (\lambda (t: T).(\forall (x4:
92 T).(\forall (x5: T).((eq T t (THead (Bind Abst) x4 x5)) \to (ex3_2 T T
93 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Abst) u2 t5))))
94 (\lambda (u2: T).(\lambda (_: T).(pr3 c x4 u2))) (\lambda (_: T).(\lambda
95 (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x5
96 t5)))))))))) H3 (THead (Bind Abst) x2 x3) H7) in (let H11 \def (H10 x2 x3
97 (refl_equal T (THead (Bind Abst) x2 x3))) in (ex3_2_ind T T (\lambda (u2:
98 T).(\lambda (t5: T).(eq T t4 (THead (Bind Abst) u2 t5)))) (\lambda (u2:
99 T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda (t5: T).(\forall
100 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x3 t5))))) (ex3_2 T T
101 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Abst) u2 t5))))
102 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
103 (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x1 t5))))))
104 (\lambda (x4: T).(\lambda (x5: T).(\lambda (H12: (eq T t4 (THead (Bind Abst)
105 x4 x5))).(\lambda (H13: (pr3 c x2 x4)).(\lambda (H14: ((\forall (b:
106 B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x3 x5))))).(ex3_2_intro T T
107 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Abst) u2 t5))))
108 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
109 (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x1 t5)))))
110 x4 x5 H12 (pr3_sing c x2 x0 H8 x4 H13) (\lambda (b: B).(\lambda (u:
111 T).(pr3_sing (CHead c (Bind b) u) x3 x1 (H9 b u) x5 (H14 b u))))))))))
112 H11)))))))) H6)))))))))))) y x H0))))) H))))).
117 theorem pr3_gen_cast:
118 \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
119 (THead (Flat Cast) u1 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda
120 (t2: T).(eq T x (THead (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_:
121 T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 c t1 t2)))) (pr3 c
124 \lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda
125 (H: (pr3 c (THead (Flat Cast) u1 t1) x)).(insert_eq T (THead (Flat Cast) u1
126 t1) (\lambda (t: T).(pr3 c t x)) (\lambda (_: T).(or (ex3_2 T T (\lambda (u2:
127 T).(\lambda (t2: T).(eq T x (THead (Flat Cast) u2 t2)))) (\lambda (u2:
128 T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 c t1
129 t2)))) (pr3 c t1 x))) (\lambda (y: T).(\lambda (H0: (pr3 c y x)).(unintro T
130 t1 (\lambda (t: T).((eq T y (THead (Flat Cast) u1 t)) \to (or (ex3_2 T T
131 (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Flat Cast) u2 t2))))
132 (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda
133 (t2: T).(pr3 c t t2)))) (pr3 c t x)))) (unintro T u1 (\lambda (t: T).(\forall
134 (x0: T).((eq T y (THead (Flat Cast) t x0)) \to (or (ex3_2 T T (\lambda (u2:
135 T).(\lambda (t2: T).(eq T x (THead (Flat Cast) u2 t2)))) (\lambda (u2:
136 T).(\lambda (_: T).(pr3 c t u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 c x0
137 t2)))) (pr3 c x0 x))))) (pr3_ind c (\lambda (t: T).(\lambda (t0: T).(\forall
138 (x0: T).(\forall (x1: T).((eq T t (THead (Flat Cast) x0 x1)) \to (or (ex3_2 T
139 T (\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Flat Cast) u2 t2))))
140 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
141 (t2: T).(pr3 c x1 t2)))) (pr3 c x1 t0))))))) (\lambda (t: T).(\lambda (x0:
142 T).(\lambda (x1: T).(\lambda (H1: (eq T t (THead (Flat Cast) x0
143 x1))).(eq_ind_r T (THead (Flat Cast) x0 x1) (\lambda (t0: T).(or (ex3_2 T T
144 (\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Flat Cast) u2 t2))))
145 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
146 (t2: T).(pr3 c x1 t2)))) (pr3 c x1 t0))) (or_introl (ex3_2 T T (\lambda (u2:
147 T).(\lambda (t2: T).(eq T (THead (Flat Cast) x0 x1) (THead (Flat Cast) u2
148 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
149 T).(\lambda (t2: T).(pr3 c x1 t2)))) (pr3 c x1 (THead (Flat Cast) x0 x1))
150 (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Flat Cast)
151 x0 x1) (THead (Flat Cast) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c
152 x0 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 c x1 t2))) x0 x1 (refl_equal T
153 (THead (Flat Cast) x0 x1)) (pr3_refl c x0) (pr3_refl c x1))) t H1)))))
154 (\lambda (t2: T).(\lambda (t3: T).(\lambda (H1: (pr2 c t3 t2)).(\lambda (t4:
155 T).(\lambda (H2: (pr3 c t2 t4)).(\lambda (H3: ((\forall (x0: T).(\forall (x1:
156 T).((eq T t2 (THead (Flat Cast) x0 x1)) \to (or (ex3_2 T T (\lambda (u2:
157 T).(\lambda (t5: T).(eq T t4 (THead (Flat Cast) u2 t5)))) (\lambda (u2:
158 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x1
159 t5)))) (pr3 c x1 t4))))))).(\lambda (x0: T).(\lambda (x1: T).(\lambda (H4:
160 (eq T t3 (THead (Flat Cast) x0 x1))).(let H5 \def (eq_ind T t3 (\lambda (t:
161 T).(pr2 c t t2)) H1 (THead (Flat Cast) x0 x1) H4) in (let H6 \def
162 (pr2_gen_cast c x0 x1 t2 H5) in (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda
163 (t5: T).(eq T t2 (THead (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_:
164 T).(pr2 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr2 c x1 t5)))) (pr2 c
165 x1 t2) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat
166 Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
167 T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t4)) (\lambda (H7: (ex3_2 T T
168 (\lambda (u2: T).(\lambda (t5: T).(eq T t2 (THead (Flat Cast) u2 t5))))
169 (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2))) (\lambda (_: T).(\lambda
170 (t5: T).(pr2 c x1 t5))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t5:
171 T).(eq T t2 (THead (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_:
172 T).(pr2 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr2 c x1 t5))) (or
173 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Cast) u2
174 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
175 T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t4)) (\lambda (x2: T).(\lambda
176 (x3: T).(\lambda (H8: (eq T t2 (THead (Flat Cast) x2 x3))).(\lambda (H9: (pr2
177 c x0 x2)).(\lambda (H10: (pr2 c x1 x3)).(let H11 \def (eq_ind T t2 (\lambda
178 (t: T).(\forall (x4: T).(\forall (x5: T).((eq T t (THead (Flat Cast) x4 x5))
179 \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat
180 Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x4 u2))) (\lambda (_:
181 T).(\lambda (t5: T).(pr3 c x5 t5)))) (pr3 c x5 t4)))))) H3 (THead (Flat Cast)
182 x2 x3) H8) in (let H12 \def (H11 x2 x3 (refl_equal T (THead (Flat Cast) x2
183 x3))) in (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead
184 (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x2 u2)))
185 (\lambda (_: T).(\lambda (t5: T).(pr3 c x3 t5)))) (pr3 c x3 t4) (or (ex3_2 T
186 T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Cast) u2 t5))))
187 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
188 (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t4)) (\lambda (H13: (ex3_2 T T (\lambda
189 (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Cast) u2 t5)))) (\lambda (u2:
190 T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x3
191 t5))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead
192 (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x2 u2)))
193 (\lambda (_: T).(\lambda (t5: T).(pr3 c x3 t5))) (or (ex3_2 T T (\lambda (u2:
194 T).(\lambda (t5: T).(eq T t4 (THead (Flat Cast) u2 t5)))) (\lambda (u2:
195 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x1
196 t5)))) (pr3 c x1 t4)) (\lambda (x4: T).(\lambda (x5: T).(\lambda (H14: (eq T
197 t4 (THead (Flat Cast) x4 x5))).(\lambda (H15: (pr3 c x2 x4)).(\lambda (H16:
198 (pr3 c x3 x5)).(eq_ind_r T (THead (Flat Cast) x4 x5) (\lambda (t: T).(or
199 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t (THead (Flat Cast) u2
200 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
201 T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t))) (or_introl (ex3_2 T T
202 (\lambda (u2: T).(\lambda (t5: T).(eq T (THead (Flat Cast) x4 x5) (THead
203 (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
204 (\lambda (_: T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 (THead (Flat
205 Cast) x4 x5)) (ex3_2_intro T T (\lambda (u2: T).(\lambda (t5: T).(eq T (THead
206 (Flat Cast) x4 x5) (THead (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_:
207 T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x1 t5))) x4 x5
208 (refl_equal T (THead (Flat Cast) x4 x5)) (pr3_sing c x2 x0 H9 x4 H15)
209 (pr3_sing c x3 x1 H10 x5 H16))) t4 H14)))))) H13)) (\lambda (H13: (pr3 c x3
210 t4)).(or_intror (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead
211 (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
212 (\lambda (_: T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t4) (pr3_sing c
213 x3 x1 H10 t4 H13))) H12)))))))) H7)) (\lambda (H7: (pr2 c x1 t2)).(or_intror
214 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Cast) u2
215 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
216 T).(\lambda (t5: T).(pr3 c x1 t5)))) (pr3 c x1 t4) (pr3_sing c t2 x1 H7 t4
217 H2))) H6)))))))))))) y x H0))))) H))))).
222 theorem pr3_gen_lift:
223 \forall (c: C).(\forall (t1: T).(\forall (x: T).(\forall (h: nat).(\forall
224 (d: nat).((pr3 c (lift h d t1) x) \to (\forall (e: C).((drop h d c e) \to
225 (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2: T).(pr3 e t1
228 \lambda (c: C).(\lambda (t1: T).(\lambda (x: T).(\lambda (h: nat).(\lambda
229 (d: nat).(\lambda (H: (pr3 c (lift h d t1) x)).(insert_eq T (lift h d t1)
230 (\lambda (t: T).(pr3 c t x)) (\lambda (_: T).(\forall (e: C).((drop h d c e)
231 \to (ex2 T (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2: T).(pr3 e
232 t1 t2)))))) (\lambda (y: T).(\lambda (H0: (pr3 c y x)).(unintro T t1 (\lambda
233 (t: T).((eq T y (lift h d t)) \to (\forall (e: C).((drop h d c e) \to (ex2 T
234 (\lambda (t2: T).(eq T x (lift h d t2))) (\lambda (t2: T).(pr3 e t t2)))))))
235 (pr3_ind c (\lambda (t: T).(\lambda (t0: T).(\forall (x0: T).((eq T t (lift h
236 d x0)) \to (\forall (e: C).((drop h d c e) \to (ex2 T (\lambda (t2: T).(eq T
237 t0 (lift h d t2))) (\lambda (t2: T).(pr3 e x0 t2))))))))) (\lambda (t:
238 T).(\lambda (x0: T).(\lambda (H1: (eq T t (lift h d x0))).(\lambda (e:
239 C).(\lambda (_: (drop h d c e)).(ex_intro2 T (\lambda (t2: T).(eq T t (lift h
240 d t2))) (\lambda (t2: T).(pr3 e x0 t2)) x0 H1 (pr3_refl e x0))))))) (\lambda
241 (t2: T).(\lambda (t3: T).(\lambda (H1: (pr2 c t3 t2)).(\lambda (t4:
242 T).(\lambda (_: (pr3 c t2 t4)).(\lambda (H3: ((\forall (x0: T).((eq T t2
243 (lift h d x0)) \to (\forall (e: C).((drop h d c e) \to (ex2 T (\lambda (t5:
244 T).(eq T t4 (lift h d t5))) (\lambda (t5: T).(pr3 e x0 t5))))))))).(\lambda
245 (x0: T).(\lambda (H4: (eq T t3 (lift h d x0))).(\lambda (e: C).(\lambda (H5:
246 (drop h d c e)).(let H6 \def (eq_ind T t3 (\lambda (t: T).(pr2 c t t2)) H1
247 (lift h d x0) H4) in (let H7 \def (pr2_gen_lift c x0 t2 h d H6 e H5) in
248 (ex2_ind T (\lambda (t5: T).(eq T t2 (lift h d t5))) (\lambda (t5: T).(pr2 e
249 x0 t5)) (ex2 T (\lambda (t5: T).(eq T t4 (lift h d t5))) (\lambda (t5:
250 T).(pr3 e x0 t5))) (\lambda (x1: T).(\lambda (H8: (eq T t2 (lift h d
251 x1))).(\lambda (H9: (pr2 e x0 x1)).(ex2_ind T (\lambda (t5: T).(eq T t4 (lift
252 h d t5))) (\lambda (t5: T).(pr3 e x1 t5)) (ex2 T (\lambda (t5: T).(eq T t4
253 (lift h d t5))) (\lambda (t5: T).(pr3 e x0 t5))) (\lambda (x2: T).(\lambda
254 (H10: (eq T t4 (lift h d x2))).(\lambda (H11: (pr3 e x1 x2)).(ex_intro2 T
255 (\lambda (t5: T).(eq T t4 (lift h d t5))) (\lambda (t5: T).(pr3 e x0 t5)) x2
256 H10 (pr3_sing e x1 x0 H9 x2 H11))))) (H3 x1 H8 e H5))))) H7))))))))))))) y x
262 theorem pr3_gen_lref:
263 \forall (c: C).(\forall (x: T).(\forall (n: nat).((pr3 c (TLRef n) x) \to
264 (or (eq T x (TLRef n)) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda
265 (_: T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
266 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
267 (v: T).(eq T x (lift (S n) O v))))))))))
269 \lambda (c: C).(\lambda (x: T).(\lambda (n: nat).(\lambda (H: (pr3 c (TLRef
270 n) x)).(insert_eq T (TLRef n) (\lambda (t: T).(pr3 c t x)) (\lambda (t:
271 T).(or (eq T x t) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_:
272 T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
273 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
274 (v: T).(eq T x (lift (S n) O v)))))))) (\lambda (y: T).(\lambda (H0: (pr3 c y
275 x)).(pr3_ind c (\lambda (t: T).(\lambda (t0: T).((eq T t (TLRef n)) \to (or
276 (eq T t0 t) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_:
277 T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
278 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
279 (v: T).(eq T t0 (lift (S n) O v)))))))))) (\lambda (t: T).(\lambda (_: (eq T
280 t (TLRef n))).(or_introl (eq T t t) (ex3_3 C T T (\lambda (d: C).(\lambda (u:
281 T).(\lambda (_: T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d:
282 C).(\lambda (u: T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda
283 (_: T).(\lambda (v: T).(eq T t (lift (S n) O v)))))) (refl_equal T t))))
284 (\lambda (t2: T).(\lambda (t1: T).(\lambda (H1: (pr2 c t1 t2)).(\lambda (t3:
285 T).(\lambda (H2: (pr3 c t2 t3)).(\lambda (H3: (((eq T t2 (TLRef n)) \to (or
286 (eq T t3 t2) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_:
287 T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
288 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
289 (v: T).(eq T t3 (lift (S n) O v)))))))))).(\lambda (H4: (eq T t1 (TLRef
290 n))).(let H5 \def (eq_ind T t1 (\lambda (t: T).(pr2 c t t2)) H1 (TLRef n) H4)
291 in (eq_ind_r T (TLRef n) (\lambda (t: T).(or (eq T t3 t) (ex3_3 C T T
292 (\lambda (d: C).(\lambda (u: T).(\lambda (_: T).(getl n c (CHead d (Bind
293 Abbr) u))))) (\lambda (d: C).(\lambda (u: T).(\lambda (v: T).(pr3 d u v))))
294 (\lambda (_: C).(\lambda (_: T).(\lambda (v: T).(eq T t3 (lift (S n) O
295 v)))))))) (let H6 \def (pr2_gen_lref c t2 n H5) in (or_ind (eq T t2 (TLRef
296 n)) (ex2_2 C T (\lambda (d: C).(\lambda (u: T).(getl n c (CHead d (Bind Abbr)
297 u)))) (\lambda (_: C).(\lambda (u: T).(eq T t2 (lift (S n) O u))))) (or (eq T
298 t3 (TLRef n)) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_:
299 T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
300 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
301 (v: T).(eq T t3 (lift (S n) O v))))))) (\lambda (H7: (eq T t2 (TLRef
302 n))).(let H8 \def (eq_ind T t2 (\lambda (t: T).((eq T t (TLRef n)) \to (or
303 (eq T t3 t) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_:
304 T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
305 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
306 (v: T).(eq T t3 (lift (S n) O v))))))))) H3 (TLRef n) H7) in (let H9 \def
307 (eq_ind T t2 (\lambda (t: T).(pr3 c t t3)) H2 (TLRef n) H7) in (H8
308 (refl_equal T (TLRef n)))))) (\lambda (H7: (ex2_2 C T (\lambda (d:
309 C).(\lambda (u: T).(getl n c (CHead d (Bind Abbr) u)))) (\lambda (_:
310 C).(\lambda (u: T).(eq T t2 (lift (S n) O u)))))).(ex2_2_ind C T (\lambda (d:
311 C).(\lambda (u: T).(getl n c (CHead d (Bind Abbr) u)))) (\lambda (_:
312 C).(\lambda (u: T).(eq T t2 (lift (S n) O u)))) (or (eq T t3 (TLRef n))
313 (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_: T).(getl n c (CHead
314 d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u: T).(\lambda (v: T).(pr3 d u
315 v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (v: T).(eq T t3 (lift (S n) O
316 v))))))) (\lambda (x0: C).(\lambda (x1: T).(\lambda (H8: (getl n c (CHead x0
317 (Bind Abbr) x1))).(\lambda (H9: (eq T t2 (lift (S n) O x1))).(let H10 \def
318 (eq_ind T t2 (\lambda (t: T).((eq T t (TLRef n)) \to (or (eq T t3 t) (ex3_3 C
319 T T (\lambda (d: C).(\lambda (u: T).(\lambda (_: T).(getl n c (CHead d (Bind
320 Abbr) u))))) (\lambda (d: C).(\lambda (u: T).(\lambda (v: T).(pr3 d u v))))
321 (\lambda (_: C).(\lambda (_: T).(\lambda (v: T).(eq T t3 (lift (S n) O
322 v))))))))) H3 (lift (S n) O x1) H9) in (let H11 \def (eq_ind T t2 (\lambda
323 (t: T).(pr3 c t t3)) H2 (lift (S n) O x1) H9) in (let H12 \def (pr3_gen_lift
324 c x1 t3 (S n) O H11 x0 (getl_drop Abbr c x0 x1 n H8)) in (ex2_ind T (\lambda
325 (t4: T).(eq T t3 (lift (S n) O t4))) (\lambda (t4: T).(pr3 x0 x1 t4)) (or (eq
326 T t3 (TLRef n)) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_:
327 T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u:
328 T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda
329 (v: T).(eq T t3 (lift (S n) O v))))))) (\lambda (x2: T).(\lambda (H13: (eq T
330 t3 (lift (S n) O x2))).(\lambda (H14: (pr3 x0 x1 x2)).(or_intror (eq T t3
331 (TLRef n)) (ex3_3 C T T (\lambda (d: C).(\lambda (u: T).(\lambda (_: T).(getl
332 n c (CHead d (Bind Abbr) u))))) (\lambda (d: C).(\lambda (u: T).(\lambda (v:
333 T).(pr3 d u v)))) (\lambda (_: C).(\lambda (_: T).(\lambda (v: T).(eq T t3
334 (lift (S n) O v)))))) (ex3_3_intro C T T (\lambda (d: C).(\lambda (u:
335 T).(\lambda (_: T).(getl n c (CHead d (Bind Abbr) u))))) (\lambda (d:
336 C).(\lambda (u: T).(\lambda (v: T).(pr3 d u v)))) (\lambda (_: C).(\lambda
337 (_: T).(\lambda (v: T).(eq T t3 (lift (S n) O v))))) x0 x1 x2 H8 H14 H13)))))
338 H12)))))))) H7)) H6)) t1 H4))))))))) y x H0))) H)))).
343 theorem pr3_gen_void:
344 \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
345 (THead (Bind Void) u1 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda
346 (t2: T).(eq T x (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_:
347 T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall
348 (u: T).(pr3 (CHead c (Bind b) u) t1 t2)))))) (pr3 (CHead c (Bind Void) u1) t1
349 (lift (S O) O x)))))))
351 \lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda
352 (H: (pr3 c (THead (Bind Void) u1 t1) x)).(insert_eq T (THead (Bind Void) u1
353 t1) (\lambda (t: T).(pr3 c t x)) (\lambda (_: T).(or (ex3_2 T T (\lambda (u2:
354 T).(\lambda (t2: T).(eq T x (THead (Bind Void) u2 t2)))) (\lambda (u2:
355 T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall
356 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) t1 t2)))))) (pr3 (CHead c
357 (Bind Void) u1) t1 (lift (S O) O x)))) (\lambda (y: T).(\lambda (H0: (pr3 c y
358 x)).(unintro T t1 (\lambda (t: T).((eq T y (THead (Bind Void) u1 t)) \to (or
359 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Bind Void) u2
360 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_:
361 T).(\lambda (t2: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
362 t t2)))))) (pr3 (CHead c (Bind Void) u1) t (lift (S O) O x))))) (unintro T u1
363 (\lambda (t: T).(\forall (x0: T).((eq T y (THead (Bind Void) t x0)) \to (or
364 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Bind Void) u2
365 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c t u2))) (\lambda (_:
366 T).(\lambda (t2: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
367 x0 t2)))))) (pr3 (CHead c (Bind Void) t) x0 (lift (S O) O x)))))) (pr3_ind c
368 (\lambda (t: T).(\lambda (t0: T).(\forall (x0: T).(\forall (x1: T).((eq T t
369 (THead (Bind Void) x0 x1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
370 T).(eq T t0 (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_:
371 T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall
372 (u: T).(pr3 (CHead c (Bind b) u) x1 t2)))))) (pr3 (CHead c (Bind Void) x0) x1
373 (lift (S O) O t0)))))))) (\lambda (t: T).(\lambda (x0: T).(\lambda (x1:
374 T).(\lambda (H1: (eq T t (THead (Bind Void) x0 x1))).(eq_ind_r T (THead (Bind
375 Void) x0 x1) (\lambda (t0: T).(or (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
376 T).(eq T t0 (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_:
377 T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall
378 (u: T).(pr3 (CHead c (Bind b) u) x1 t2)))))) (pr3 (CHead c (Bind Void) x0) x1
379 (lift (S O) O t0)))) (or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
380 T).(eq T (THead (Bind Void) x0 x1) (THead (Bind Void) u2 t2)))) (\lambda (u2:
381 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall
382 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x1 t2)))))) (pr3 (CHead c
383 (Bind Void) x0) x1 (lift (S O) O (THead (Bind Void) x0 x1))) (ex3_2_intro T T
384 (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Bind Void) x0 x1) (THead
385 (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
386 (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead
387 c (Bind b) u) x1 t2))))) x0 x1 (refl_equal T (THead (Bind Void) x0 x1))
388 (pr3_refl c x0) (\lambda (b: B).(\lambda (u: T).(pr3_refl (CHead c (Bind b)
389 u) x1))))) t H1))))) (\lambda (t2: T).(\lambda (t3: T).(\lambda (H1: (pr2 c
390 t3 t2)).(\lambda (t4: T).(\lambda (H2: (pr3 c t2 t4)).(\lambda (H3: ((\forall
391 (x0: T).(\forall (x1: T).((eq T t2 (THead (Bind Void) x0 x1)) \to (or (ex3_2
392 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Void) u2 t5))))
393 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
394 (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x1 t5))))))
395 (pr3 (CHead c (Bind Void) x0) x1 (lift (S O) O t4)))))))).(\lambda (x0:
396 T).(\lambda (x1: T).(\lambda (H4: (eq T t3 (THead (Bind Void) x0 x1))).(let
397 H5 \def (eq_ind T t3 (\lambda (t: T).(pr2 c t t2)) H1 (THead (Bind Void) x0
398 x1) H4) in (let H6 \def (pr2_gen_void c x0 x1 t2 H5) in (or_ind (ex3_2 T T
399 (\lambda (u2: T).(\lambda (t5: T).(eq T t2 (THead (Bind Void) u2 t5))))
400 (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2))) (\lambda (_: T).(\lambda
401 (t5: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x1 t5))))))
402 (\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x1 (lift (S O) O
403 t2)))) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind
404 Void) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
405 T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
406 x1 t5)))))) (pr3 (CHead c (Bind Void) x0) x1 (lift (S O) O t4))) (\lambda
407 (H7: (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t2 (THead (Bind Void)
408 u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2))) (\lambda (_:
409 T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
410 x1 t5))))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t5: T).(eq T t2 (THead
411 (Bind Void) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2)))
412 (\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead
413 c (Bind b) u) x1 t5))))) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq
414 T t4 (THead (Bind Void) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0
415 u2))) (\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3
416 (CHead c (Bind b) u) x1 t5)))))) (pr3 (CHead c (Bind Void) x0) x1 (lift (S O)
417 O t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H8: (eq T t2 (THead (Bind
418 Void) x2 x3))).(\lambda (H9: (pr2 c x0 x2)).(\lambda (H10: ((\forall (b:
419 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x1 x3))))).(let H11 \def (eq_ind
420 T t2 (\lambda (t: T).(\forall (x4: T).(\forall (x5: T).((eq T t (THead (Bind
421 Void) x4 x5)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4
422 (THead (Bind Void) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x4 u2)))
423 (\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead
424 c (Bind b) u) x5 t5)))))) (pr3 (CHead c (Bind Void) x4) x5 (lift (S O) O
425 t4))))))) H3 (THead (Bind Void) x2 x3) H8) in (let H12 \def (H11 x2 x3
426 (refl_equal T (THead (Bind Void) x2 x3))) in (or_ind (ex3_2 T T (\lambda (u2:
427 T).(\lambda (t5: T).(eq T t4 (THead (Bind Void) u2 t5)))) (\lambda (u2:
428 T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda (t5: T).(\forall
429 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x3 t5)))))) (pr3 (CHead c
430 (Bind Void) x2) x3 (lift (S O) O t4)) (or (ex3_2 T T (\lambda (u2:
431 T).(\lambda (t5: T).(eq T t4 (THead (Bind Void) u2 t5)))) (\lambda (u2:
432 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(\forall
433 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x1 t5)))))) (pr3 (CHead c
434 (Bind Void) x0) x1 (lift (S O) O t4))) (\lambda (H13: (ex3_2 T T (\lambda
435 (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Void) u2 t5)))) (\lambda (u2:
436 T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda (t5: T).(\forall
437 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x3 t5))))))).(ex3_2_ind T T
438 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Void) u2 t5))))
439 (\lambda (u2: T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda
440 (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x3 t5)))))
441 (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Void)
442 u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
443 T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
444 x1 t5)))))) (pr3 (CHead c (Bind Void) x0) x1 (lift (S O) O t4))) (\lambda
445 (x4: T).(\lambda (x5: T).(\lambda (H14: (eq T t4 (THead (Bind Void) x4
446 x5))).(\lambda (H15: (pr3 c x2 x4)).(\lambda (H16: ((\forall (b: B).(\forall
447 (u: T).(pr3 (CHead c (Bind b) u) x3 x5))))).(or_introl (ex3_2 T T (\lambda
448 (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Void) u2 t5)))) (\lambda (u2:
449 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(\forall
450 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x1 t5)))))) (pr3 (CHead c
451 (Bind Void) x0) x1 (lift (S O) O t4)) (ex3_2_intro T T (\lambda (u2:
452 T).(\lambda (t5: T).(eq T t4 (THead (Bind Void) u2 t5)))) (\lambda (u2:
453 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(\forall
454 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x1 t5))))) x4 x5 H14
455 (pr3_sing c x2 x0 H9 x4 H15) (\lambda (b: B).(\lambda (u: T).(pr3_sing (CHead
456 c (Bind b) u) x3 x1 (H10 b u) x5 (H16 b u))))))))))) H13)) (\lambda (H13:
457 (pr3 (CHead c (Bind Void) x2) x3 (lift (S O) O t4))).(or_intror (ex3_2 T T
458 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Void) u2 t5))))
459 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
460 (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x1 t5))))))
461 (pr3 (CHead c (Bind Void) x0) x1 (lift (S O) O t4)) (pr3_sing (CHead c (Bind
462 Void) x0) x3 x1 (H10 Void x0) (lift (S O) O t4) (pr3_pr2_pr3_t c x2 x3 (lift
463 (S O) O t4) (Bind Void) H13 x0 H9)))) H12)))))))) H7)) (\lambda (H7:
464 ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x1 (lift (S O) O
465 t2)))))).(or_intror (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4
466 (THead (Bind Void) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
467 (\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead
468 c (Bind b) u) x1 t5)))))) (pr3 (CHead c (Bind Void) x0) x1 (lift (S O) O t4))
469 (pr3_sing (CHead c (Bind Void) x0) (lift (S O) O t2) x1 (H7 Void x0) (lift (S
470 O) O t4) (pr3_lift (CHead c (Bind Void) x0) c (S O) O (drop_drop (Bind Void)
471 O c c (drop_refl c) x0) t2 t4 H2)))) H6)))))))))))) y x H0))))) H))))).
476 theorem pr3_gen_abbr:
477 \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
478 (THead (Bind Abbr) u1 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda
479 (t2: T).(eq T x (THead (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_:
480 T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind Abbr)
481 u1) t1 t2)))) (pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O x)))))))
483 \lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda
484 (H: (pr3 c (THead (Bind Abbr) u1 t1) x)).(insert_eq T (THead (Bind Abbr) u1
485 t1) (\lambda (t: T).(pr3 c t x)) (\lambda (_: T).(or (ex3_2 T T (\lambda (u2:
486 T).(\lambda (t2: T).(eq T x (THead (Bind Abbr) u2 t2)))) (\lambda (u2:
487 T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3
488 (CHead c (Bind Abbr) u1) t1 t2)))) (pr3 (CHead c (Bind Abbr) u1) t1 (lift (S
489 O) O x)))) (\lambda (y: T).(\lambda (H0: (pr3 c y x)).(unintro T t1 (\lambda
490 (t: T).((eq T y (THead (Bind Abbr) u1 t)) \to (or (ex3_2 T T (\lambda (u2:
491 T).(\lambda (t2: T).(eq T x (THead (Bind Abbr) u2 t2)))) (\lambda (u2:
492 T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3
493 (CHead c (Bind Abbr) u1) t t2)))) (pr3 (CHead c (Bind Abbr) u1) t (lift (S O)
494 O x))))) (unintro T u1 (\lambda (t: T).(\forall (x0: T).((eq T y (THead (Bind
495 Abbr) t x0)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x
496 (THead (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c t u2)))
497 (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind Abbr) t) x0 t2)))) (pr3
498 (CHead c (Bind Abbr) t) x0 (lift (S O) O x)))))) (pr3_ind c (\lambda (t:
499 T).(\lambda (t0: T).(\forall (x0: T).(\forall (x1: T).((eq T t (THead (Bind
500 Abbr) x0 x1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T t0
501 (THead (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
502 (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind Abbr) x0) x1 t2)))) (pr3
503 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t0)))))))) (\lambda (t: T).(\lambda
504 (x0: T).(\lambda (x1: T).(\lambda (H1: (eq T t (THead (Bind Abbr) x0
505 x1))).(eq_ind_r T (THead (Bind Abbr) x0 x1) (\lambda (t0: T).(or (ex3_2 T T
506 (\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Bind Abbr) u2 t2))))
507 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
508 (t2: T).(pr3 (CHead c (Bind Abbr) x0) x1 t2)))) (pr3 (CHead c (Bind Abbr) x0)
509 x1 (lift (S O) O t0)))) (or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
510 T).(eq T (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 t2)))) (\lambda (u2:
511 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3
512 (CHead c (Bind Abbr) x0) x1 t2)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S
513 O) O (THead (Bind Abbr) x0 x1))) (ex3_2_intro T T (\lambda (u2: T).(\lambda
514 (t2: T).(eq T (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 t2)))) (\lambda
515 (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3
516 (CHead c (Bind Abbr) x0) x1 t2))) x0 x1 (refl_equal T (THead (Bind Abbr) x0
517 x1)) (pr3_refl c x0) (pr3_refl (CHead c (Bind Abbr) x0) x1))) t H1)))))
518 (\lambda (t2: T).(\lambda (t3: T).(\lambda (H1: (pr2 c t3 t2)).(\lambda (t4:
519 T).(\lambda (H2: (pr3 c t2 t4)).(\lambda (H3: ((\forall (x0: T).(\forall (x1:
520 T).((eq T t2 (THead (Bind Abbr) x0 x1)) \to (or (ex3_2 T T (\lambda (u2:
521 T).(\lambda (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2:
522 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
523 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S
524 O) O t4)))))))).(\lambda (x0: T).(\lambda (x1: T).(\lambda (H4: (eq T t3
525 (THead (Bind Abbr) x0 x1))).(let H5 \def (eq_ind T t3 (\lambda (t: T).(pr2 c
526 t t2)) H1 (THead (Bind Abbr) x0 x1) H4) in (let H6 \def (pr2_gen_abbr c x0 x1
527 t2 H5) in (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t2
528 (THead (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2)))
529 (\lambda (_: T).(\lambda (t5: T).(or3 (\forall (b: B).(\forall (u: T).(pr2
530 (CHead c (Bind b) u) x1 t5))) (ex2 T (\lambda (u: T).(pr0 x0 u)) (\lambda (u:
531 T).(pr2 (CHead c (Bind Abbr) u) x1 t5))) (ex3_2 T T (\lambda (y0: T).(\lambda
532 (_: T).(pr2 (CHead c (Bind Abbr) x0) x1 y0))) (\lambda (y0: T).(\lambda (z:
533 T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c (Bind Abbr) x0)
534 z t5)))))))) (\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x1
535 (lift (S O) O t2)))) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T
536 t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0
537 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x0) x1
538 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4))) (\lambda (H7:
539 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t2 (THead (Bind Abbr) u2
540 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2))) (\lambda (_:
541 T).(\lambda (t5: T).(or3 (\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind
542 b) u) x1 t5))) (ex2 T (\lambda (u: T).(pr0 x0 u)) (\lambda (u: T).(pr2 (CHead
543 c (Bind Abbr) u) x1 t5))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2
544 (CHead c (Bind Abbr) x0) x1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0
545 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c (Bind Abbr) x0) z
546 t5))))))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t5: T).(eq T t2 (THead
547 (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2)))
548 (\lambda (_: T).(\lambda (t5: T).(or3 (\forall (b: B).(\forall (u: T).(pr2
549 (CHead c (Bind b) u) x1 t5))) (ex2 T (\lambda (u: T).(pr0 x0 u)) (\lambda (u:
550 T).(pr2 (CHead c (Bind Abbr) u) x1 t5))) (ex3_2 T T (\lambda (y0: T).(\lambda
551 (_: T).(pr2 (CHead c (Bind Abbr) x0) x1 y0))) (\lambda (y0: T).(\lambda (z:
552 T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c (Bind Abbr) x0)
553 z t5))))))) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead
554 (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
555 (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3
556 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4))) (\lambda (x2: T).(\lambda
557 (x3: T).(\lambda (H8: (eq T t2 (THead (Bind Abbr) x2 x3))).(\lambda (H9: (pr2
558 c x0 x2)).(\lambda (H10: (or3 (\forall (b: B).(\forall (u: T).(pr2 (CHead c
559 (Bind b) u) x1 x3))) (ex2 T (\lambda (u: T).(pr0 x0 u)) (\lambda (u: T).(pr2
560 (CHead c (Bind Abbr) u) x1 x3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_:
561 T).(pr2 (CHead c (Bind Abbr) x0) x1 y0))) (\lambda (y0: T).(\lambda (z:
562 T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c (Bind Abbr) x0)
563 z x3)))))).(or3_ind (\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
564 x1 x3))) (ex2 T (\lambda (u: T).(pr0 x0 u)) (\lambda (u: T).(pr2 (CHead c
565 (Bind Abbr) u) x1 x3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2
566 (CHead c (Bind Abbr) x0) x1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0
567 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c (Bind Abbr) x0) z x3))))
568 (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Abbr)
569 u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
570 T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3 (CHead c
571 (Bind Abbr) x0) x1 (lift (S O) O t4))) (\lambda (H11: ((\forall (b:
572 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) x1 x3))))).(let H12 \def (eq_ind
573 T t2 (\lambda (t: T).(\forall (x4: T).(\forall (x5: T).((eq T t (THead (Bind
574 Abbr) x4 x5)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4
575 (THead (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x4 u2)))
576 (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x4) x5 t5)))) (pr3
577 (CHead c (Bind Abbr) x4) x5 (lift (S O) O t4))))))) H3 (THead (Bind Abbr) x2
578 x3) H8) in (let H13 \def (H12 x2 x3 (refl_equal T (THead (Bind Abbr) x2 x3)))
579 in (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind
580 Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_:
581 T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x2) x3 t5)))) (pr3 (CHead c
582 (Bind Abbr) x2) x3 (lift (S O) O t4)) (or (ex3_2 T T (\lambda (u2:
583 T).(\lambda (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2:
584 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
585 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S
586 O) O t4))) (\lambda (H14: (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T
587 t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x2
588 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x2) x3
589 t5))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead
590 (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x2 u2)))
591 (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x2) x3 t5))) (or
592 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Abbr) u2
593 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
594 T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3 (CHead c
595 (Bind Abbr) x0) x1 (lift (S O) O t4))) (\lambda (x4: T).(\lambda (x5:
596 T).(\lambda (H15: (eq T t4 (THead (Bind Abbr) x4 x5))).(\lambda (H16: (pr3 c
597 x2 x4)).(\lambda (H17: (pr3 (CHead c (Bind Abbr) x2) x3 x5)).(eq_ind_r T
598 (THead (Bind Abbr) x4 x5) (\lambda (t: T).(or (ex3_2 T T (\lambda (u2:
599 T).(\lambda (t5: T).(eq T t (THead (Bind Abbr) u2 t5)))) (\lambda (u2:
600 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
601 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S
602 O) O t)))) (or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T
603 (THead (Bind Abbr) x4 x5) (THead (Bind Abbr) u2 t5)))) (\lambda (u2:
604 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
605 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S
606 O) O (THead (Bind Abbr) x4 x5))) (ex3_2_intro T T (\lambda (u2: T).(\lambda
607 (t5: T).(eq T (THead (Bind Abbr) x4 x5) (THead (Bind Abbr) u2 t5)))) (\lambda
608 (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
609 (CHead c (Bind Abbr) x0) x1 t5))) x4 x5 (refl_equal T (THead (Bind Abbr) x4
610 x5)) (pr3_sing c x2 x0 H9 x4 H16) (pr3_sing (CHead c (Bind Abbr) x0) x3 x1
611 (H11 Abbr x0) x5 (pr3_pr2_pr3_t c x2 x3 x5 (Bind Abbr) H17 x0 H9)))) t4
612 H15)))))) H14)) (\lambda (H14: (pr3 (CHead c (Bind Abbr) x2) x3 (lift (S O) O
613 t4))).(or_intror (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead
614 (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
615 (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3
616 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)) (pr3_sing (CHead c (Bind Abbr)
617 x0) x3 x1 (H11 Abbr x0) (lift (S O) O t4) (pr3_pr2_pr3_t c x2 x3 (lift (S O)
618 O t4) (Bind Abbr) H14 x0 H9)))) H13)))) (\lambda (H11: (ex2 T (\lambda (u:
619 T).(pr0 x0 u)) (\lambda (u: T).(pr2 (CHead c (Bind Abbr) u) x1
620 x3)))).(ex2_ind T (\lambda (u: T).(pr0 x0 u)) (\lambda (u: T).(pr2 (CHead c
621 (Bind Abbr) u) x1 x3)) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T
622 t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0
623 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x0) x1
624 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4))) (\lambda (x4:
625 T).(\lambda (H12: (pr0 x0 x4)).(\lambda (H13: (pr2 (CHead c (Bind Abbr) x4)
626 x1 x3)).(let H14 \def (eq_ind T t2 (\lambda (t: T).(\forall (x5: T).(\forall
627 (x6: T).((eq T t (THead (Bind Abbr) x5 x6)) \to (or (ex3_2 T T (\lambda (u2:
628 T).(\lambda (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2:
629 T).(\lambda (_: T).(pr3 c x5 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
630 (CHead c (Bind Abbr) x5) x6 t5)))) (pr3 (CHead c (Bind Abbr) x5) x6 (lift (S
631 O) O t4))))))) H3 (THead (Bind Abbr) x2 x3) H8) in (let H15 \def (H14 x2 x3
632 (refl_equal T (THead (Bind Abbr) x2 x3))) in (or_ind (ex3_2 T T (\lambda (u2:
633 T).(\lambda (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2:
634 T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
635 (CHead c (Bind Abbr) x2) x3 t5)))) (pr3 (CHead c (Bind Abbr) x2) x3 (lift (S
636 O) O t4)) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead
637 (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
638 (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3
639 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4))) (\lambda (H16: (ex3_2 T T
640 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5))))
641 (\lambda (u2: T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda
642 (t5: T).(pr3 (CHead c (Bind Abbr) x2) x3 t5))))).(ex3_2_ind T T (\lambda (u2:
643 T).(\lambda (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2:
644 T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
645 (CHead c (Bind Abbr) x2) x3 t5))) (or (ex3_2 T T (\lambda (u2: T).(\lambda
646 (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_:
647 T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr)
648 x0) x1 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4))) (\lambda
649 (x5: T).(\lambda (x6: T).(\lambda (H17: (eq T t4 (THead (Bind Abbr) x5
650 x6))).(\lambda (H18: (pr3 c x2 x5)).(\lambda (H19: (pr3 (CHead c (Bind Abbr)
651 x2) x3 x6)).(eq_ind_r T (THead (Bind Abbr) x5 x6) (\lambda (t: T).(or (ex3_2
652 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t (THead (Bind Abbr) u2 t5))))
653 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
654 (t5: T).(pr3 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3 (CHead c (Bind Abbr) x0)
655 x1 (lift (S O) O t)))) (or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t5:
656 T).(eq T (THead (Bind Abbr) x5 x6) (THead (Bind Abbr) u2 t5)))) (\lambda (u2:
657 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
658 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S
659 O) O (THead (Bind Abbr) x5 x6))) (ex3_2_intro T T (\lambda (u2: T).(\lambda
660 (t5: T).(eq T (THead (Bind Abbr) x5 x6) (THead (Bind Abbr) u2 t5)))) (\lambda
661 (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
662 (CHead c (Bind Abbr) x0) x1 t5))) x5 x6 (refl_equal T (THead (Bind Abbr) x5
663 x6)) (pr3_sing c x2 x0 H9 x5 H18) (pr3_t x3 x1 (CHead c (Bind Abbr) x0)
664 (pr3_pr0_pr2_t x0 x4 H12 c x1 x3 (Bind Abbr) H13) x6 (pr3_pr2_pr3_t c x2 x3
665 x6 (Bind Abbr) H19 x0 H9)))) t4 H17)))))) H16)) (\lambda (H16: (pr3 (CHead c
666 (Bind Abbr) x2) x3 (lift (S O) O t4))).(or_intror (ex3_2 T T (\lambda (u2:
667 T).(\lambda (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2:
668 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
669 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S
670 O) O t4)) (pr3_t x3 x1 (CHead c (Bind Abbr) x0) (pr3_pr0_pr2_t x0 x4 H12 c x1
671 x3 (Bind Abbr) H13) (lift (S O) O t4) (pr3_pr2_pr3_t c x2 x3 (lift (S O) O
672 t4) (Bind Abbr) H16 x0 H9)))) H15)))))) H11)) (\lambda (H11: (ex3_2 T T
673 (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c (Bind Abbr) x0) x1 y0)))
674 (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z:
675 T).(pr2 (CHead c (Bind Abbr) x0) z x3))))).(ex3_2_ind T T (\lambda (y0:
676 T).(\lambda (_: T).(pr2 (CHead c (Bind Abbr) x0) x1 y0))) (\lambda (y0:
677 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c
678 (Bind Abbr) x0) z x3))) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq
679 T t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0
680 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x0) x1
681 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4))) (\lambda (x4:
682 T).(\lambda (x5: T).(\lambda (H12: (pr2 (CHead c (Bind Abbr) x0) x1
683 x4)).(\lambda (H13: (pr0 x4 x5)).(\lambda (H14: (pr2 (CHead c (Bind Abbr) x0)
684 x5 x3)).(let H15 \def (eq_ind T t2 (\lambda (t: T).(\forall (x6: T).(\forall
685 (x7: T).((eq T t (THead (Bind Abbr) x6 x7)) \to (or (ex3_2 T T (\lambda (u2:
686 T).(\lambda (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2:
687 T).(\lambda (_: T).(pr3 c x6 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
688 (CHead c (Bind Abbr) x6) x7 t5)))) (pr3 (CHead c (Bind Abbr) x6) x7 (lift (S
689 O) O t4))))))) H3 (THead (Bind Abbr) x2 x3) H8) in (let H16 \def (H15 x2 x3
690 (refl_equal T (THead (Bind Abbr) x2 x3))) in (or_ind (ex3_2 T T (\lambda (u2:
691 T).(\lambda (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2:
692 T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
693 (CHead c (Bind Abbr) x2) x3 t5)))) (pr3 (CHead c (Bind Abbr) x2) x3 (lift (S
694 O) O t4)) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead
695 (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
696 (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3
697 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4))) (\lambda (H17: (ex3_2 T T
698 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5))))
699 (\lambda (u2: T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda
700 (t5: T).(pr3 (CHead c (Bind Abbr) x2) x3 t5))))).(ex3_2_ind T T (\lambda (u2:
701 T).(\lambda (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2:
702 T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
703 (CHead c (Bind Abbr) x2) x3 t5))) (or (ex3_2 T T (\lambda (u2: T).(\lambda
704 (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_:
705 T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr)
706 x0) x1 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4))) (\lambda
707 (x6: T).(\lambda (x7: T).(\lambda (H18: (eq T t4 (THead (Bind Abbr) x6
708 x7))).(\lambda (H19: (pr3 c x2 x6)).(\lambda (H20: (pr3 (CHead c (Bind Abbr)
709 x2) x3 x7)).(eq_ind_r T (THead (Bind Abbr) x6 x7) (\lambda (t: T).(or (ex3_2
710 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t (THead (Bind Abbr) u2 t5))))
711 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
712 (t5: T).(pr3 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3 (CHead c (Bind Abbr) x0)
713 x1 (lift (S O) O t)))) (or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t5:
714 T).(eq T (THead (Bind Abbr) x6 x7) (THead (Bind Abbr) u2 t5)))) (\lambda (u2:
715 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
716 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S
717 O) O (THead (Bind Abbr) x6 x7))) (ex3_2_intro T T (\lambda (u2: T).(\lambda
718 (t5: T).(eq T (THead (Bind Abbr) x6 x7) (THead (Bind Abbr) u2 t5)))) (\lambda
719 (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3
720 (CHead c (Bind Abbr) x0) x1 t5))) x6 x7 (refl_equal T (THead (Bind Abbr) x6
721 x7)) (pr3_sing c x2 x0 H9 x6 H19) (pr3_sing (CHead c (Bind Abbr) x0) x4 x1
722 H12 x7 (pr3_sing (CHead c (Bind Abbr) x0) x5 x4 (pr2_free (CHead c (Bind
723 Abbr) x0) x4 x5 H13) x7 (pr3_sing (CHead c (Bind Abbr) x0) x3 x5 H14 x7
724 (pr3_pr2_pr3_t c x2 x3 x7 (Bind Abbr) H20 x0 H9)))))) t4 H18)))))) H17))
725 (\lambda (H17: (pr3 (CHead c (Bind Abbr) x2) x3 (lift (S O) O
726 t4))).(or_intror (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead
727 (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
728 (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr) x0) x1 t5)))) (pr3
729 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)) (pr3_sing (CHead c (Bind Abbr)
730 x0) x4 x1 H12 (lift (S O) O t4) (pr3_sing (CHead c (Bind Abbr) x0) x5 x4
731 (pr2_free (CHead c (Bind Abbr) x0) x4 x5 H13) (lift (S O) O t4) (pr3_sing
732 (CHead c (Bind Abbr) x0) x3 x5 H14 (lift (S O) O t4) (pr3_pr2_pr3_t c x2 x3
733 (lift (S O) O t4) (Bind Abbr) H17 x0 H9)))))) H16)))))))) H11)) H10))))))
734 H7)) (\lambda (H7: ((\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
735 x1 (lift (S O) O t2)))))).(or_intror (ex3_2 T T (\lambda (u2: T).(\lambda
736 (t5: T).(eq T t4 (THead (Bind Abbr) u2 t5)))) (\lambda (u2: T).(\lambda (_:
737 T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 (CHead c (Bind Abbr)
738 x0) x1 t5)))) (pr3 (CHead c (Bind Abbr) x0) x1 (lift (S O) O t4)) (pr3_sing
739 (CHead c (Bind Abbr) x0) (lift (S O) O t2) x1 (H7 Abbr x0) (lift (S O) O t4)
740 (pr3_lift (CHead c (Bind Abbr) x0) c (S O) O (drop_drop (Bind Abbr) O c c
741 (drop_refl c) x0) t2 t4 H2)))) H6)))))))))))) y x H0))))) H))))).
746 theorem pr3_gen_appl:
747 \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c
748 (THead (Flat Appl) u1 t1) x) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda
749 (t2: T).(eq T x (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_:
750 T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 c t1 t2)))) (ex4_4 T
751 T T T (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2: T).(pr3
752 c (THead (Bind Abbr) u2 t2) x))))) (\lambda (_: T).(\lambda (_: T).(\lambda
753 (u2: T).(\lambda (_: T).(pr3 c u1 u2))))) (\lambda (y1: T).(\lambda (z1:
754 T).(\lambda (_: T).(\lambda (_: T).(pr3 c t1 (THead (Bind Abst) y1 z1))))))
755 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2: T).(\forall
756 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1 t2)))))))) (ex6_6 B T T T
757 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
758 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
759 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3
760 c t1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
761 (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind
762 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) x))))))) (\lambda (_:
763 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
764 (_: T).(pr3 c u1 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
765 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
766 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
767 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2)))))))))))))
769 \lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda
770 (H: (pr3 c (THead (Flat Appl) u1 t1) x)).(insert_eq T (THead (Flat Appl) u1
771 t1) (\lambda (t: T).(pr3 c t x)) (\lambda (_: T).(or3 (ex3_2 T T (\lambda
772 (u2: T).(\lambda (t2: T).(eq T x (THead (Flat Appl) u2 t2)))) (\lambda (u2:
773 T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 c t1
774 t2)))) (ex4_4 T T T T (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
775 T).(\lambda (t2: T).(pr3 c (THead (Bind Abbr) u2 t2) x))))) (\lambda (_:
776 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2)))))
777 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(pr3 c t1
778 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
779 T).(\lambda (t2: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
780 z1 t2)))))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
781 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
782 (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
783 (_: T).(\lambda (_: T).(pr3 c t1 (THead (Bind b) y1 z1)))))))) (\lambda (b:
784 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
785 (y2: T).(pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))
786 x))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
787 T).(\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2))))))) (\lambda (_:
788 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
789 (y2: T).(pr3 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
790 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b)
791 y2) z1 z2)))))))))) (\lambda (y: T).(\lambda (H0: (pr3 c y x)).(unintro T t1
792 (\lambda (t: T).((eq T y (THead (Flat Appl) u1 t)) \to (or3 (ex3_2 T T
793 (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Flat Appl) u2 t2))))
794 (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda
795 (t2: T).(pr3 c t t2)))) (ex4_4 T T T T (\lambda (_: T).(\lambda (_:
796 T).(\lambda (u2: T).(\lambda (t2: T).(pr3 c (THead (Bind Abbr) u2 t2) x)))))
797 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c u1
798 u2))))) (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
799 T).(pr3 c t (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1:
800 T).(\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall (u: T).(pr3
801 (CHead c (Bind b) u) z1 t2)))))))) (ex6_6 B T T T T T (\lambda (b:
802 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
803 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
804 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c t (THead (Bind
805 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
806 (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b) y2 (THead
807 (Flat Appl) (lift (S O) O u2) z2)) x))))))) (\lambda (_: B).(\lambda (_:
808 T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c u1
809 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
810 T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2))))))) (\lambda (b:
811 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda
812 (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))))) (unintro T u1 (\lambda
813 (t: T).(\forall (x0: T).((eq T y (THead (Flat Appl) t x0)) \to (or3 (ex3_2 T
814 T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Flat Appl) u2 t2))))
815 (\lambda (u2: T).(\lambda (_: T).(pr3 c t u2))) (\lambda (_: T).(\lambda (t2:
816 T).(pr3 c x0 t2)))) (ex4_4 T T T T (\lambda (_: T).(\lambda (_: T).(\lambda
817 (u2: T).(\lambda (t2: T).(pr3 c (THead (Bind Abbr) u2 t2) x))))) (\lambda (_:
818 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c t u2))))) (\lambda
819 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(pr3 c x0 (THead
820 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
821 T).(\lambda (t2: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
822 z1 t2)))))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
823 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
824 (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
825 (_: T).(\lambda (_: T).(pr3 c x0 (THead (Bind b) y1 z1)))))))) (\lambda (b:
826 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
827 (y2: T).(pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))
828 x))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
829 T).(\lambda (u2: T).(\lambda (_: T).(pr3 c t u2))))))) (\lambda (_:
830 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
831 (y2: T).(pr3 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
832 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b)
833 y2) z1 z2)))))))))))) (pr3_ind c (\lambda (t: T).(\lambda (t0: T).(\forall
834 (x0: T).(\forall (x1: T).((eq T t (THead (Flat Appl) x0 x1)) \to (or3 (ex3_2
835 T T (\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Flat Appl) u2 t2))))
836 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
837 (t2: T).(pr3 c x1 t2)))) (ex4_4 T T T T (\lambda (_: T).(\lambda (_:
838 T).(\lambda (u2: T).(\lambda (t2: T).(pr3 c (THead (Bind Abbr) u2 t2) t0)))))
839 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0
840 u2))))) (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
841 T).(pr3 c x1 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1:
842 T).(\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall (u: T).(pr3
843 (CHead c (Bind b) u) z1 t2)))))))) (ex6_6 B T T T T T (\lambda (b:
844 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
845 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
846 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead
847 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
848 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b)
849 y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t0))))))) (\lambda (_:
850 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
851 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
852 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
853 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
854 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))))))))
855 (\lambda (t: T).(\lambda (x0: T).(\lambda (x1: T).(\lambda (H1: (eq T t
856 (THead (Flat Appl) x0 x1))).(eq_ind_r T (THead (Flat Appl) x0 x1) (\lambda
857 (t0: T).(or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead
858 (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
859 (\lambda (_: T).(\lambda (t2: T).(pr3 c x1 t2)))) (ex4_4 T T T T (\lambda (_:
860 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2: T).(pr3 c (THead (Bind
861 Abbr) u2 t2) t0))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
862 T).(\lambda (_: T).(pr3 c x0 u2))))) (\lambda (y1: T).(\lambda (z1:
863 T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead (Bind Abst) y1 z1))))))
864 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t2: T).(\forall
865 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1 t2)))))))) (ex6_6 B T T T
866 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
867 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
868 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3
869 c x1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
870 (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind
871 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t0))))))) (\lambda (_:
872 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
873 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
874 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
875 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
876 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))))
877 (or3_intro0 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Flat
878 Appl) x0 x1) (THead (Flat Appl) u2 t2)))) (\lambda (u2: T).(\lambda (_:
879 T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 c x1 t2)))) (ex4_4 T
880 T T T (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t2: T).(pr3
881 c (THead (Bind Abbr) u2 t2) (THead (Flat Appl) x0 x1)))))) (\lambda (_:
882 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))))
883 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1
884 (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 b) u)
886 z1 t2)))))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
887 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
888 (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
889 (_: T).(\lambda (_: T).(pr3 c x1 (THead (Bind b) y1 z1)))))))) (\lambda (b:
890 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
891 (y2: T).(pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))
892 (THead (Flat Appl) x0 x1)))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
893 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))))))
894 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
895 T).(\lambda (y2: T).(pr3 c y1 y2))))))) (\lambda (b: B).(\lambda (_:
896 T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr3
897 (CHead c (Bind b) y2) z1 z2)))))))) (ex3_2_intro T T (\lambda (u2:
898 T).(\lambda (t2: T).(eq T (THead (Flat Appl) x0 x1) (THead (Flat Appl) u2
899 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
900 T).(\lambda (t2: T).(pr3 c x1 t2))) x0 x1 (refl_equal T (THead (Flat Appl) x0
901 x1)) (pr3_refl c x0) (pr3_refl c x1))) t H1))))) (\lambda (t2: T).(\lambda
902 (t3: T).(\lambda (H1: (pr2 c t3 t2)).(\lambda (t4: T).(\lambda (H2: (pr3 c t2
903 t4)).(\lambda (H3: ((\forall (x0: T).(\forall (x1: T).((eq T t2 (THead (Flat
904 Appl) x0 x1)) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4
905 (THead (Flat Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
906 (\lambda (_: T).(\lambda (t5: T).(pr3 c x1 t5)))) (ex4_4 T T T T (\lambda (_:
907 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind
908 Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
909 T).(\lambda (_: T).(pr3 c x0 u2))))) (\lambda (y1: T).(\lambda (z1:
910 T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead (Bind Abst) y1 z1))))))
911 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t5: T).(\forall
912 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T
913 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
914 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
915 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3
916 c x1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
917 (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind
918 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
919 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
920 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
921 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
922 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
923 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1
924 z2)))))))))))))).(\lambda (x0: T).(\lambda (x1: T).(\lambda (H4: (eq T t3
925 (THead (Flat Appl) x0 x1))).(let H5 \def (eq_ind T t3 (\lambda (t: T).(pr2 c
926 t t2)) H1 (THead (Flat Appl) x0 x1) H4) in (let H6 \def (pr2_gen_appl c x0 x1
927 t2 H5) in (or3_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t2
928 (THead (Flat Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2)))
929 (\lambda (_: T).(\lambda (t5: T).(pr2 c x1 t5)))) (ex4_4 T T T T (\lambda
930 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(eq T x1 (THead
931 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
932 T).(\lambda (t5: T).(eq T t2 (THead (Bind Abbr) u2 t5)))))) (\lambda (_:
933 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2)))))
934 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t5: T).(\forall
935 (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T
936 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
937 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
938 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq
939 T x1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
940 (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead
941 (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
942 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
943 (_: T).(pr2 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
944 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
945 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
946 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))) (or3 (ex3_2
947 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Appl) u2 t5))))
948 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
949 (t5: T).(pr3 c x1 t5)))) (ex4_4 T T T T (\lambda (_: T).(\lambda (_:
950 T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind Abbr) u2 t5) t4)))))
951 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0
952 u2))))) (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
953 T).(pr3 c x1 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1:
954 T).(\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3
955 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T T T (\lambda (b:
956 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
957 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
958 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead
959 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
960 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b)
961 y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
962 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
963 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
964 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
965 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
966 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))) (\lambda
967 (H7: (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t2 (THead (Flat Appl)
968 u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c x0 u2))) (\lambda (_:
969 T).(\lambda (t5: T).(pr2 c x1 t5))))).(ex3_2_ind T T (\lambda (u2:
970 T).(\lambda (t5: T).(eq T t2 (THead (Flat Appl) u2 t5)))) (\lambda (u2:
971 T).(\lambda (_: T).(pr2 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr2 c x1
972 t5))) (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat
973 Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
974 T).(\lambda (t5: T).(pr3 c x1 t5)))) (ex4_4 T T T T (\lambda (_: T).(\lambda
975 (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind Abbr) u2 t5)
976 t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3
977 c x0 u2))))) (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
978 T).(pr3 c x1 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1:
979 T).(\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3
980 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T T T (\lambda (b:
981 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
982 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
983 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead
984 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
985 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b)
986 y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
987 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
988 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
989 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
990 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
991 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))) (\lambda
992 (x2: T).(\lambda (x3: T).(\lambda (H8: (eq T t2 (THead (Flat Appl) x2
993 x3))).(\lambda (H9: (pr2 c x0 x2)).(\lambda (H10: (pr2 c x1 x3)).(let H11
994 \def (eq_ind T t2 (\lambda (t: T).(\forall (x4: T).(\forall (x5: T).((eq T t
995 (THead (Flat Appl) x4 x5)) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t5:
996 T).(eq T t4 (THead (Flat Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_:
997 T).(pr3 c x4 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x5 t5)))) (ex4_4 T
998 T T T (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3
999 c (THead (Bind Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda
1000 (u2: T).(\lambda (_: T).(pr3 c x4 u2))))) (\lambda (y1: T).(\lambda (z1:
1001 T).(\lambda (_: T).(\lambda (_: T).(pr3 c x5 (THead (Bind Abst) y1 z1))))))
1002 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t5: T).(\forall
1003 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T
1004 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1005 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
1006 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3
1007 c x5 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
1008 (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind
1009 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
1010 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1011 (_: T).(pr3 c x4 u2))))))) (\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))))))))))))) H3
1015 (THead (Flat Appl) x2 x3) H8) in (let H12 \def (eq_ind T t2 (\lambda (t:
1016 T).(pr3 c t t4)) H2 (THead (Flat Appl) x2 x3) H8) in (let H13 \def (H11 x2 x3
1017 (refl_equal T (THead (Flat Appl) x2 x3))) in (or3_ind (ex3_2 T T (\lambda
1018 (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Appl) u2 t5)))) (\lambda (u2:
1019 T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x3
1020 t5)))) (ex4_4 T T T T (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1021 T).(\lambda (t5: T).(pr3 c (THead (Bind Abbr) u2 t5) t4))))) (\lambda (_:
1022 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x2 u2)))))
1023 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(pr3 c x3
1024 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1025 T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
1026 z1 t5)))))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
1027 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
1028 (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
1029 (_: T).(\lambda (_: T).(pr3 c x3 (THead (Bind b) y1 z1)))))))) (\lambda (b:
1030 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
1031 (y2: T).(pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))
1032 t4))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1033 T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x2 u2))))))) (\lambda (_:
1034 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1035 (y2: T).(pr3 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
1036 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b)
1037 y2) z1 z2)))))))) (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4
1038 (THead (Flat Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
1039 (\lambda (_: T).(\lambda (t5: T).(pr3 c x1 t5)))) (ex4_4 T T T T (\lambda (_:
1040 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind
1041 Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1042 T).(\lambda (_: T).(pr3 c x0 u2))))) (\lambda (y1: T).(\lambda (z1:
1043 T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead (Bind Abst) y1 z1))))))
1044 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t5: T).(\forall
1045 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T
1046 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1047 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
1048 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3
1049 c x1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
1050 (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind
1051 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
1052 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1053 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1054 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
1055 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1056 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))) (\lambda
1057 (H14: (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat
1058 Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_:
1059 T).(\lambda (t5: T).(pr3 c x3 t5))))).(ex3_2_ind T T (\lambda (u2:
1060 T).(\lambda (t5: T).(eq T t4 (THead (Flat Appl) u2 t5)))) (\lambda (u2:
1061 T).(\lambda (_: T).(pr3 c x2 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x3
1062 t5))) (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat
1063 Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
1064 T).(\lambda (t5: T).(pr3 c x1 t5)))) (ex4_4 T T T T (\lambda (_: T).(\lambda
1065 (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind Abbr) u2 t5)
1066 t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3
1067 c x0 u2))))) (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
1068 T).(pr3 c x1 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1:
1069 T).(\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3
1070 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T T T (\lambda (b:
1071 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1072 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
1073 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead
1074 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
1075 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b)
1076 y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
1077 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1078 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1079 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
1080 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1081 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))) (\lambda
1082 (x4: T).(\lambda (x5: T).(\lambda (H15: (eq T t4 (THead (Flat Appl) x4
1083 x5))).(\lambda (H16: (pr3 c x2 x4)).(\lambda (H17: (pr3 c x3 x5)).(eq_ind_r T
1084 (THead (Flat Appl) x4 x5) (\lambda (t: T).(or3 (ex3_2 T T (\lambda (u2:
1085 T).(\lambda (t5: T).(eq T t (THead (Flat Appl) u2 t5)))) (\lambda (u2:
1086 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x1
1087 t5)))) (ex4_4 T T T T (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1088 T).(\lambda (t5: T).(pr3 c (THead (Bind Abbr) u2 t5) t))))) (\lambda (_:
1089 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))))
1090 (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1
1091 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1092 T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
1093 z1 t5)))))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
1094 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
1095 (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
1096 (_: T).(\lambda (_: T).(pr3 c x1 (THead (Bind b) y1 z1)))))))) (\lambda (b:
1097 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
1098 (y2: T).(pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))
1099 t))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1100 T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))))))) (\lambda (_:
1101 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1102 (y2: T).(pr3 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
1103 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b)
1104 y2) z1 z2)))))))))) (or3_intro0 (ex3_2 T T (\lambda (u2: T).(\lambda (t5:
1105 T).(eq T (THead (Flat Appl) x4 x5) (THead (Flat Appl) u2 t5)))) (\lambda (u2:
1106 T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x1
1107 t5)))) (ex4_4 T T T T (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1108 T).(\lambda (t5: T).(pr3 c (THead (Bind Abbr) u2 t5) (THead (Flat Appl) x4
1109 x5)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_:
1110 T).(pr3 c x0 u2))))) (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
1111 T).(\lambda (_: T).(pr3 c x1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
1112 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall
1113 (u: T).(pr3 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T T T (\lambda
1114 (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1115 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
1116 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1
1117 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
1118 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b)
1119 y2 (THead (Flat Appl) (lift (S O) O u2) z2)) (THead (Flat Appl) x4 x5))))))))
1120 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1121 T).(\lambda (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1:
1122 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1
1123 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
1124 T).(\lambda (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))
1125 (ex3_2_intro T T (\lambda (u2: T).(\lambda (t5: T).(eq T (THead (Flat Appl)
1126 x4 x5) (THead (Flat Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c
1127 x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x1 t5))) x4 x5 (refl_equal T
1128 (THead (Flat Appl) x4 x5)) (pr3_sing c x2 x0 H9 x4 H16) (pr3_sing c x3 x1 H10
1129 x5 H17))) t4 H15)))))) H14)) (\lambda (H14: (ex4_4 T T T T (\lambda (_:
1130 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind
1131 Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1132 T).(\lambda (_: T).(pr3 c x2 u2))))) (\lambda (y1: T).(\lambda (z1:
1133 T).(\lambda (_: T).(\lambda (_: T).(pr3 c x3 (THead (Bind Abst) y1 z1))))))
1134 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t5: T).(\forall
1135 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1 t5))))))))).(ex4_4_ind T
1136 T T T (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3
1137 c (THead (Bind Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda
1138 (u2: T).(\lambda (_: T).(pr3 c x2 u2))))) (\lambda (y1: T).(\lambda (z1:
1139 T).(\lambda (_: T).(\lambda (_: T).(pr3 c x3 (THead (Bind Abst) y1 z1))))))
1140 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t5: T).(\forall
1141 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1 t5))))))) (or3 (ex3_2 T T
1142 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Appl) u2 t5))))
1143 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
1144 (t5: T).(pr3 c x1 t5)))) (ex4_4 T T T T (\lambda (_: T).(\lambda (_:
1145 T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind Abbr) u2 t5) t4)))))
1146 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0
1147 u2))))) (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
1148 T).(pr3 c x1 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1:
1149 T).(\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3
1150 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T T T (\lambda (b:
1151 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1152 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
1153 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead
1154 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
1155 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b)
1156 y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
1157 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1158 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1159 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
1160 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1161 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))) (\lambda
1162 (x4: T).(\lambda (x5: T).(\lambda (x6: T).(\lambda (x7: T).(\lambda (H15:
1163 (pr3 c (THead (Bind Abbr) x6 x7) t4)).(\lambda (H16: (pr3 c x2 x6)).(\lambda
1164 (H17: (pr3 c x3 (THead (Bind Abst) x4 x5))).(\lambda (H18: ((\forall (b:
1165 B).(\forall (u: T).(pr3 (CHead c (Bind b) u) x5 x7))))).(or3_intro1 (ex3_2 T
1166 T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Appl) u2 t5))))
1167 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
1168 (t5: T).(pr3 c x1 t5)))) (ex4_4 T T T T (\lambda (_: T).(\lambda (_:
1169 T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind Abbr) u2 t5) t4)))))
1170 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0
1171 u2))))) (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
1172 T).(pr3 c x1 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1:
1173 T).(\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3
1174 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T T T (\lambda (b:
1175 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1176 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
1177 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead
1178 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
1179 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b)
1180 y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
1181 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1182 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1183 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
1184 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1185 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2)))))))) (ex4_4_intro
1186 T T T T (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5:
1187 T).(pr3 c (THead (Bind Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_:
1188 T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))))) (\lambda (y1:
1189 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead (Bind
1190 Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
1191 (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1
1192 t5))))))) x4 x5 x6 x7 H15 (pr3_sing c x2 x0 H9 x6 H16) (pr3_sing c x3 x1 H10
1193 (THead (Bind Abst) x4 x5) H17) H18)))))))))) H14)) (\lambda (H14: (ex6_6 B T
1194 T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1195 T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
1196 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1197 (_: T).(pr3 c x3 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
1198 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c
1199 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4)))))))
1200 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1201 T).(\lambda (_: T).(pr3 c x2 u2))))))) (\lambda (_: B).(\lambda (y1:
1202 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1
1203 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
1204 T).(\lambda (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1
1205 z2))))))))).(ex6_6_ind B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda
1206 (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b
1207 Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
1208 T).(\lambda (_: T).(\lambda (_: T).(pr3 c x3 (THead (Bind b) y1 z1))))))))
1209 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda
1210 (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift
1211 (S O) O u2) z2)) t4))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_:
1212 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x2 u2)))))))
1213 (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1214 T).(\lambda (y2: T).(pr3 c y1 y2))))))) (\lambda (b: B).(\lambda (_:
1215 T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr3
1216 (CHead c (Bind b) y2) z1 z2))))))) (or3 (ex3_2 T T (\lambda (u2: T).(\lambda
1217 (t5: T).(eq T t4 (THead (Flat Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_:
1218 T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x1 t5)))) (ex4_4 T
1219 T T T (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3
1220 c (THead (Bind Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda
1221 (u2: T).(\lambda (_: T).(pr3 c x0 u2))))) (\lambda (y1: T).(\lambda (z1:
1222 T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead (Bind Abst) y1 z1))))))
1223 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t5: T).(\forall
1224 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T
1225 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1226 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
1227 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3
1228 c x1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
1229 (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind
1230 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
1231 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1232 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1233 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
1234 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1235 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))) (\lambda
1236 (x4: B).(\lambda (x5: T).(\lambda (x6: T).(\lambda (x7: T).(\lambda (x8:
1237 T).(\lambda (x9: T).(\lambda (H15: (not (eq B x4 Abst))).(\lambda (H16: (pr3
1238 c x3 (THead (Bind x4) x5 x6))).(\lambda (H17: (pr3 c (THead (Bind x4) x9
1239 (THead (Flat Appl) (lift (S O) O x8) x7)) t4)).(\lambda (H18: (pr3 c x2
1240 x8)).(\lambda (H19: (pr3 c x5 x9)).(\lambda (H20: (pr3 (CHead c (Bind x4) x9)
1241 x6 x7)).(or3_intro2 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4
1242 (THead (Flat Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
1243 (\lambda (_: T).(\lambda (t5: T).(pr3 c x1 t5)))) (ex4_4 T T T T (\lambda (_:
1244 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind
1245 Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1246 T).(\lambda (_: T).(pr3 c x0 u2))))) (\lambda (y1: T).(\lambda (z1:
1247 T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead (Bind Abst) y1 z1))))))
1248 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t5: T).(\forall
1249 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T
1250 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1251 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
1252 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3
1253 c x1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
1254 (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind
1255 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
1256 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1257 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1258 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
1259 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1260 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2)))))))) (ex6_6_intro
1261 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1262 T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
1263 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1264 (_: T).(pr3 c x1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
1265 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c
1266 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4)))))))
1267 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1268 T).(\lambda (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1:
1269 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1
1270 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
1271 T).(\lambda (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2)))))))
1272 x4 x5 x6 x7 x8 x9 H15 (pr3_sing c x3 x1 H10 (THead (Bind x4) x5 x6) H16) H17
1273 (pr3_sing c x2 x0 H9 x8 H18) H19 H20)))))))))))))) H14)) H13))))))))) H7))
1274 (\lambda (H7: (ex4_4 T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda (_:
1275 T).(\lambda (_: T).(eq T x1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
1276 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(eq T t2 (THead (Bind
1277 Abbr) u2 t5)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1278 (_: T).(pr2 c x0 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1279 T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
1280 z1 t5))))))))).(ex4_4_ind T T T T (\lambda (y1: T).(\lambda (z1: T).(\lambda
1281 (_: T).(\lambda (_: T).(eq T x1 (THead (Bind Abst) y1 z1)))))) (\lambda (_:
1282 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(eq T t2 (THead (Bind
1283 Abbr) u2 t5)))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1284 (_: T).(pr2 c x0 u2))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1285 T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u)
1286 z1 t5))))))) (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4
1287 (THead (Flat Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2)))
1288 (\lambda (_: T).(\lambda (t5: T).(pr3 c x1 t5)))) (ex4_4 T T T T (\lambda (_:
1289 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind
1290 Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1291 T).(\lambda (_: T).(pr3 c x0 u2))))) (\lambda (y1: T).(\lambda (z1:
1292 T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead (Bind Abst) y1 z1))))))
1293 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t5: T).(\forall
1294 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T
1295 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1296 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
1297 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3
1298 c x1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
1299 (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind
1300 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
1301 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1302 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1303 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
1304 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1305 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))) (\lambda
1306 (x2: T).(\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda (H8: (eq
1307 T x1 (THead (Bind Abst) x2 x3))).(\lambda (H9: (eq T t2 (THead (Bind Abbr) x4
1308 x5))).(\lambda (H10: (pr2 c x0 x4)).(\lambda (H11: ((\forall (b: B).(\forall
1309 (u: T).(pr2 (CHead c (Bind b) u) x3 x5))))).(eq_ind_r T (THead (Bind Abst) x2
1310 x3) (\lambda (t: T).(or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T
1311 t4 (THead (Flat Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0
1312 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c t t5)))) (ex4_4 T T T T
1313 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c
1314 (THead (Bind Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda
1315 (u2: T).(\lambda (_: T).(pr3 c x0 u2))))) (\lambda (y1: T).(\lambda (z1:
1316 T).(\lambda (_: T).(\lambda (_: T).(pr3 c t (THead (Bind Abst) y1 z1))))))
1317 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t5: T).(\forall
1318 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T
1319 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1320 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
1321 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3
1322 c t (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
1323 (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind
1324 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
1325 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1326 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1327 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
1328 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1329 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2)))))))))) (let H12
1330 \def (eq_ind T t2 (\lambda (t: T).(\forall (x6: T).(\forall (x7: T).((eq T t
1331 (THead (Flat Appl) x6 x7)) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t5:
1332 T).(eq T t4 (THead (Flat Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_:
1333 T).(pr3 c x6 u2))) (\lambda (_: T).(\lambda (t5: T).(pr3 c x7 t5)))) (ex4_4 T
1334 T T T (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3
1335 c (THead (Bind Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda
1336 (u2: T).(\lambda (_: T).(pr3 c x6 u2))))) (\lambda (y1: T).(\lambda (z1:
1337 T).(\lambda (_: T).(\lambda (_: T).(pr3 c x7 (THead (Bind Abst) y1 z1))))))
1338 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t5: T).(\forall
1339 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T
1340 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1341 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
1342 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3
1343 c x7 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
1344 (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind
1345 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
1346 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1347 (_: T).(pr3 c x6 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1348 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
1349 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1350 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))))))) H3
1351 (THead (Bind Abbr) x4 x5) H9) in (let H13 \def (eq_ind T t2 (\lambda (t:
1352 T).(pr3 c t t4)) H2 (THead (Bind Abbr) x4 x5) H9) in (or3_intro1 (ex3_2 T T
1353 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Appl) u2 t5))))
1354 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
1355 (t5: T).(pr3 c (THead (Bind Abst) x2 x3) t5)))) (ex4_4 T T T T (\lambda (_:
1356 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind
1357 Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1358 T).(\lambda (_: T).(pr3 c x0 u2))))) (\lambda (y1: T).(\lambda (z1:
1359 T).(\lambda (_: T).(\lambda (_: T).(pr3 c (THead (Bind Abst) x2 x3) (THead
1360 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1361 T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
1362 z1 t5)))))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
1363 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
1364 (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
1365 (_: T).(\lambda (_: T).(pr3 c (THead (Bind Abst) x2 x3) (THead (Bind b) y1
1366 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2:
1367 T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b) y2 (THead (Flat
1368 Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_: B).(\lambda (_:
1369 T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0
1370 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
1371 T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2))))))) (\lambda (b:
1372 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda
1373 (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2)))))))) (ex4_4_intro T T T T
1374 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c
1375 (THead (Bind Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda
1376 (u2: T).(\lambda (_: T).(pr3 c x0 u2))))) (\lambda (y1: T).(\lambda (z1:
1377 T).(\lambda (_: T).(\lambda (_: T).(pr3 c (THead (Bind Abst) x2 x3) (THead
1378 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1379 T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
1380 z1 t5))))))) x2 x3 x4 x5 H13 (pr3_pr2 c x0 x4 H10) (pr3_refl c (THead (Bind
1381 Abst) x2 x3)) (\lambda (b: B).(\lambda (u: T).(pr3_pr2 (CHead c (Bind b) u)
1382 x3 x5 (H11 b u)))))))) x1 H8))))))))) H7)) (\lambda (H7: (ex6_6 B T T T T T
1383 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1384 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
1385 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(eq T x1
1386 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
1387 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T t2 (THead (Bind
1388 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))))))))) (\lambda (_:
1389 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1390 (_: T).(pr2 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1391 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1 y2)))))))
1392 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1393 (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2))))))))).(ex6_6_ind
1394 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1395 T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b:
1396 B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1397 (_: T).(eq T x1 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_:
1398 T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(eq T
1399 t2 (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)))))))))
1400 (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1401 T).(\lambda (_: T).(pr2 c x0 u2))))))) (\lambda (_: B).(\lambda (y1:
1402 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr2 c y1
1403 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2:
1404 T).(\lambda (_: T).(\lambda (y2: T).(pr2 (CHead c (Bind b) y2) z1 z2)))))))
1405 (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Appl)
1406 u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_:
1407 T).(\lambda (t5: T).(pr3 c x1 t5)))) (ex4_4 T T T T (\lambda (_: T).(\lambda
1408 (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind Abbr) u2 t5)
1409 t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3
1410 c x0 u2))))) (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
1411 T).(pr3 c x1 (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1:
1412 T).(\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3
1413 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T T T (\lambda (b:
1414 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1415 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
1416 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c x1 (THead
1417 (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_:
1418 T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b)
1419 y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
1420 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1421 (_: T).(pr3 c x0 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1422 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
1423 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1424 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))) (\lambda
1425 (x2: B).(\lambda (x3: T).(\lambda (x4: T).(\lambda (x5: T).(\lambda (x6:
1426 T).(\lambda (x7: T).(\lambda (H8: (not (eq B x2 Abst))).(\lambda (H9: (eq T
1427 x1 (THead (Bind x2) x3 x4))).(\lambda (H10: (eq T t2 (THead (Bind x2) x7
1428 (THead (Flat Appl) (lift (S O) O x6) x5)))).(\lambda (H11: (pr2 c x0
1429 x6)).(\lambda (H12: (pr2 c x3 x7)).(\lambda (H13: (pr2 (CHead c (Bind x2) x7)
1430 x4 x5)).(eq_ind_r T (THead (Bind x2) x3 x4) (\lambda (t: T).(or3 (ex3_2 T T
1431 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Appl) u2 t5))))
1432 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
1433 (t5: T).(pr3 c t t5)))) (ex4_4 T T T T (\lambda (_: T).(\lambda (_:
1434 T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind Abbr) u2 t5) t4)))))
1435 (\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0
1436 u2))))) (\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_:
1437 T).(pr3 c t (THead (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1:
1438 T).(\lambda (_: T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3
1439 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T T T (\lambda (b:
1440 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1441 (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1: T).(\lambda
1442 (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c t (THead (Bind
1443 b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda
1444 (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b) y2 (THead
1445 (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_: B).(\lambda (_:
1446 T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0
1447 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
1448 T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2))))))) (\lambda (b:
1449 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda
1450 (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2)))))))))) (let H14 \def (eq_ind T t2
1451 (\lambda (t: T).(\forall (x8: T).(\forall (x9: T).((eq T t (THead (Flat Appl)
1452 x8 x9)) \to (or3 (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead
1453 (Flat Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c x8 u2)))
1454 (\lambda (_: T).(\lambda (t5: T).(pr3 c x9 t5)))) (ex4_4 T T T T (\lambda (_:
1455 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind
1456 Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1457 T).(\lambda (_: T).(pr3 c x8 u2))))) (\lambda (y1: T).(\lambda (z1:
1458 T).(\lambda (_: T).(\lambda (_: T).(pr3 c x9 (THead (Bind Abst) y1 z1))))))
1459 (\lambda (_: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (t5: T).(\forall
1460 (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u) z1 t5)))))))) (ex6_6 B T T T
1461 T T (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1462 (_: T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda
1463 (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3
1464 c x9 (THead (Bind b) y1 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda
1465 (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind
1466 b) y2 (THead (Flat Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_:
1467 B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda
1468 (_: T).(pr3 c x8 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_:
1469 T).(\lambda (_: T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2)))))))
1470 (\lambda (b: B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda
1471 (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2))))))))))))) H3
1472 (THead (Bind x2) x7 (THead (Flat Appl) (lift (S O) O x6) x5)) H10) in (let
1473 H15 \def (eq_ind T t2 (\lambda (t: T).(pr3 c t t4)) H2 (THead (Bind x2) x7
1474 (THead (Flat Appl) (lift (S O) O x6) x5)) H10) in (or3_intro2 (ex3_2 T T
1475 (\lambda (u2: T).(\lambda (t5: T).(eq T t4 (THead (Flat Appl) u2 t5))))
1476 (\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))) (\lambda (_: T).(\lambda
1477 (t5: T).(pr3 c (THead (Bind x2) x3 x4) t5)))) (ex4_4 T T T T (\lambda (_:
1478 T).(\lambda (_: T).(\lambda (u2: T).(\lambda (t5: T).(pr3 c (THead (Bind
1479 Abbr) u2 t5) t4))))) (\lambda (_: T).(\lambda (_: T).(\lambda (u2:
1480 T).(\lambda (_: T).(pr3 c x0 u2))))) (\lambda (y1: T).(\lambda (z1:
1481 T).(\lambda (_: T).(\lambda (_: T).(pr3 c (THead (Bind x2) x3 x4) (THead
1482 (Bind Abst) y1 z1)))))) (\lambda (_: T).(\lambda (z1: T).(\lambda (_:
1483 T).(\lambda (t5: T).(\forall (b: B).(\forall (u: T).(pr3 (CHead c (Bind b) u)
1484 z1 t5)))))))) (ex6_6 B T T T T T (\lambda (b: B).(\lambda (_: T).(\lambda (_:
1485 T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(not (eq B b Abst))))))))
1486 (\lambda (b: B).(\lambda (y1: T).(\lambda (z1: T).(\lambda (_: T).(\lambda
1487 (_: T).(\lambda (_: T).(pr3 c (THead (Bind x2) x3 x4) (THead (Bind b) y1
1488 z1)))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2:
1489 T).(\lambda (u2: T).(\lambda (y2: T).(pr3 c (THead (Bind b) y2 (THead (Flat
1490 Appl) (lift (S O) O u2) z2)) t4))))))) (\lambda (_: B).(\lambda (_:
1491 T).(\lambda (_: T).(\lambda (_: T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0
1492 u2))))))) (\lambda (_: B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_:
1493 T).(\lambda (_: T).(\lambda (y2: T).(pr3 c y1 y2))))))) (\lambda (b:
1494 B).(\lambda (_: T).(\lambda (z1: T).(\lambda (z2: T).(\lambda (_: T).(\lambda
1495 (y2: T).(pr3 (CHead c (Bind b) y2) z1 z2)))))))) (ex6_6_intro B T T T T T
1496 (\lambda (b: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1497 T).(\lambda (_: T).(not (eq B b Abst)))))))) (\lambda (b: B).(\lambda (y1:
1498 T).(\lambda (z1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(pr3 c
1499 (THead (Bind x2) x3 x4) (THead (Bind b) y1 z1)))))))) (\lambda (b:
1500 B).(\lambda (_: T).(\lambda (_: T).(\lambda (z2: T).(\lambda (u2: T).(\lambda
1501 (y2: T).(pr3 c (THead (Bind b) y2 (THead (Flat Appl) (lift (S O) O u2) z2))
1502 t4))))))) (\lambda (_: B).(\lambda (_: T).(\lambda (_: T).(\lambda (_:
1503 T).(\lambda (u2: T).(\lambda (_: T).(pr3 c x0 u2))))))) (\lambda (_:
1504 B).(\lambda (y1: T).(\lambda (_: T).(\lambda (_: T).(\lambda (_: T).(\lambda
1505 (y2: T).(pr3 c y1 y2))))))) (\lambda (b: B).(\lambda (_: T).(\lambda (z1:
1506 T).(\lambda (z2: T).(\lambda (_: T).(\lambda (y2: T).(pr3 (CHead c (Bind b)
1507 y2) z1 z2))))))) x2 x3 x4 x5 x6 x7 H8 (pr3_refl c (THead (Bind x2) x3 x4))
1508 H15 (pr3_pr2 c x0 x6 H11) (pr3_pr2 c x3 x7 H12) (pr3_pr2 (CHead c (Bind x2)
1509 x7) x4 x5 H13))))) x1 H9))))))))))))) H7)) H6)))))))))))) y x H0))))) H))))).
1511 Initial nodes: 12691
1514 theorem pr3_gen_bind:
1515 \forall (b: B).((not (eq B b Abst)) \to (\forall (c: C).(\forall (u1:
1516 T).(\forall (t1: T).(\forall (x: T).((pr3 c (THead (Bind b) u1 t1) x) \to (or
1517 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Bind b) u2
1518 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_:
1519 T).(\lambda (t2: T).(pr3 (CHead c (Bind b) u1) t1 t2)))) (pr3 (CHead c (Bind
1520 b) u1) t1 (lift (S O) O x)))))))))
1522 \lambda (b: B).(B_ind (\lambda (b0: B).((not (eq B b0 Abst)) \to (\forall
1523 (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr3 c (THead (Bind
1524 b0) u1 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x
1525 (THead (Bind b0) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2)))
1526 (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind b0) u1) t1 t2)))) (pr3
1527 (CHead c (Bind b0) u1) t1 (lift (S O) O x)))))))))) (\lambda (_: (not (eq B
1528 Abbr Abst))).(\lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda (x:
1529 T).(\lambda (H0: (pr3 c (THead (Bind Abbr) u1 t1) x)).(let H1 \def
1530 (pr3_gen_abbr c u1 t1 x H0) in (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda
1531 (t2: T).(eq T x (THead (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_:
1532 T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind Abbr)
1533 u1) t1 t2)))) (pr3 (CHead c (Bind Abbr) u1) t1 (lift (S O) O x)) (or (ex3_2 T
1534 T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Bind Abbr) u2 t2))))
1535 (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda
1536 (t2: T).(pr3 (CHead c (Bind Abbr) u1) t1 t2)))) (pr3 (CHead c (Bind Abbr) u1)
1537 t1 (lift (S O) O x))) (\lambda (H2: (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
1538 T).(eq T x (THead (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3
1539 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind Abbr) u1) t1
1540 t2))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Bind
1541 Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_:
1542 T).(\lambda (t2: T).(pr3 (CHead c (Bind Abbr) u1) t1 t2))) (or (ex3_2 T T
1543 (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Bind Abbr) u2 t2))))
1544 (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda
1545 (t2: T).(pr3 (CHead c (Bind Abbr) u1) t1 t2)))) (pr3 (CHead c (Bind Abbr) u1)
1546 t1 (lift (S O) O x))) (\lambda (x0: T).(\lambda (x1: T).(\lambda (H3: (eq T x
1547 (THead (Bind Abbr) x0 x1))).(\lambda (H4: (pr3 c u1 x0)).(\lambda (H5: (pr3
1548 (CHead c (Bind Abbr) u1) t1 x1)).(or_introl (ex3_2 T T (\lambda (u2:
1549 T).(\lambda (t2: T).(eq T x (THead (Bind Abbr) u2 t2)))) (\lambda (u2:
1550 T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3
1551 (CHead c (Bind Abbr) u1) t1 t2)))) (pr3 (CHead c (Bind Abbr) u1) t1 (lift (S
1552 O) O x)) (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead
1553 (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2)))
1554 (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind Abbr) u1) t1 t2))) x0 x1
1555 H3 H4 H5))))))) H2)) (\lambda (H2: (pr3 (CHead c (Bind Abbr) u1) t1 (lift (S
1556 O) O x))).(or_intror (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x
1557 (THead (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2)))
1558 (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind Abbr) u1) t1 t2)))) (pr3
1559 (CHead c (Bind Abbr) u1) t1 (lift (S O) O x)) H2)) H1)))))))) (\lambda (H:
1560 (not (eq B Abst Abst))).(\lambda (c: C).(\lambda (u1: T).(\lambda (t1:
1561 T).(\lambda (x: T).(\lambda (_: (pr3 c (THead (Bind Abst) u1 t1) x)).(let H1
1562 \def (match (H (refl_equal B Abst)) in False return (\lambda (_: False).(or
1563 (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Bind Abst) u2
1564 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_:
1565 T).(\lambda (t2: T).(pr3 (CHead c (Bind Abst) u1) t1 t2)))) (pr3 (CHead c
1566 (Bind Abst) u1) t1 (lift (S O) O x)))) with []) in H1))))))) (\lambda (_:
1567 (not (eq B Void Abst))).(\lambda (c: C).(\lambda (u1: T).(\lambda (t1:
1568 T).(\lambda (x: T).(\lambda (H0: (pr3 c (THead (Bind Void) u1 t1) x)).(let H1
1569 \def (pr3_gen_void c u1 t1 x H0) in (or_ind (ex3_2 T T (\lambda (u2:
1570 T).(\lambda (t2: T).(eq T x (THead (Bind Void) u2 t2)))) (\lambda (u2:
1571 T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall
1572 (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0) u) t1 t2)))))) (pr3 (CHead c
1573 (Bind Void) u1) t1 (lift (S O) O x)) (or (ex3_2 T T (\lambda (u2: T).(\lambda
1574 (t2: T).(eq T x (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_:
1575 T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind Void)
1576 u1) t1 t2)))) (pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x))) (\lambda
1577 (H2: (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead (Bind Void)
1578 u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_:
1579 T).(\lambda (t2: T).(\forall (b0: B).(\forall (u: T).(pr3 (CHead c (Bind b0)
1580 u) t1 t2))))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t2: T).(eq T x
1581 (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2)))
1582 (\lambda (_: T).(\lambda (t2: T).(\forall (b0: B).(\forall (u: T).(pr3 (CHead
1583 c (Bind b0) u) t1 t2))))) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
1584 T).(eq T x (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3
1585 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind Void) u1) t1
1586 t2)))) (pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x))) (\lambda (x0:
1587 T).(\lambda (x1: T).(\lambda (H3: (eq T x (THead (Bind Void) x0
1588 x1))).(\lambda (H4: (pr3 c u1 x0)).(\lambda (H5: ((\forall (b0: B).(\forall
1589 (u: T).(pr3 (CHead c (Bind b0) u) t1 x1))))).(or_introl (ex3_2 T T (\lambda
1590 (u2: T).(\lambda (t2: T).(eq T x (THead (Bind Void) u2 t2)))) (\lambda (u2:
1591 T).(\lambda (_: T).(pr3 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3
1592 (CHead c (Bind Void) u1) t1 t2)))) (pr3 (CHead c (Bind Void) u1) t1 (lift (S
1593 O) O x)) (ex3_2_intro T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead
1594 (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3 c u1 u2)))
1595 (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind Void) u1) t1 t2))) x0 x1
1596 H3 H4 (H5 Void u1)))))))) H2)) (\lambda (H2: (pr3 (CHead c (Bind Void) u1) t1
1597 (lift (S O) O x))).(or_intror (ex3_2 T T (\lambda (u2: T).(\lambda (t2:
1598 T).(eq T x (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr3
1599 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr3 (CHead c (Bind Void) u1) t1
1600 t2)))) (pr3 (CHead c (Bind Void) u1) t1 (lift (S O) O x)) H2)) H1)))))))) b).