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