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