1 (**************************************************************************)
4 (* ||A|| A project by Andrea Asperti *)
6 (* ||I|| Developers: *)
7 (* ||T|| The HELM team. *)
8 (* ||A|| http://helm.cs.unibo.it *)
10 (* \ / This file is distributed under the terms of the *)
11 (* v GNU General Public License Version 2 *)
13 (**************************************************************************)
15 (* This file was automatically generated: do not edit *********************)
17 include "basic_1A/pr2/fwd.ma".
19 include "basic_1A/pr0/subst0.ma".
22 \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall
23 (u: T).(\forall (f: F).(pr2 c (THead (Flat f) u t1) (THead (Flat f) u
26 \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t1
27 t2)).(\lambda (u: T).(\lambda (f: F).(pr2_ind (\lambda (c0: C).(\lambda (t:
28 T).(\lambda (t0: T).(pr2 c0 (THead (Flat f) u t) (THead (Flat f) u t0)))))
29 (\lambda (c0: C).(\lambda (t0: T).(\lambda (t3: T).(\lambda (H0: (pr0 t0
30 t3)).(pr2_free c0 (THead (Flat f) u t0) (THead (Flat f) u t3) (pr0_comp u u
31 (pr0_refl u) t0 t3 H0 (Flat f))))))) (\lambda (c0: C).(\lambda (d:
32 C).(\lambda (u0: T).(\lambda (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind
33 Abbr) u0))).(\lambda (t0: T).(\lambda (t3: T).(\lambda (H1: (pr0 t0
34 t3)).(\lambda (t: T).(\lambda (H2: (subst0 i u0 t3 t)).(pr2_delta c0 d u0 i
35 H0 (THead (Flat f) u t0) (THead (Flat f) u t3) (pr0_comp u u (pr0_refl u) t0
36 t3 H1 (Flat f)) (THead (Flat f) u t) (subst0_snd (Flat f) u0 t t3 i H2
37 u)))))))))))) c t1 t2 H)))))).
40 \forall (c: C).(\forall (u1: T).(\forall (u2: T).((pr2 c u1 u2) \to (\forall
41 (k: K).(\forall (t: T).(pr2 c (THead k u1 t) (THead k u2 t)))))))
43 \lambda (c: C).(\lambda (u1: T).(\lambda (u2: T).(\lambda (H: (pr2 c u1
44 u2)).(\lambda (k: K).(\lambda (t: T).(pr2_ind (\lambda (c0: C).(\lambda (t0:
45 T).(\lambda (t1: T).(pr2 c0 (THead k t0 t) (THead k t1 t))))) (\lambda (c0:
46 C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pr0 t1 t2)).(pr2_free c0
47 (THead k t1 t) (THead k t2 t) (pr0_comp t1 t2 H0 t t (pr0_refl t) k))))))
48 (\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
49 (H0: (getl i c0 (CHead d (Bind Abbr) u))).(\lambda (t1: T).(\lambda (t2:
50 T).(\lambda (H1: (pr0 t1 t2)).(\lambda (t0: T).(\lambda (H2: (subst0 i u t2
51 t0)).(pr2_delta c0 d u i H0 (THead k t1 t) (THead k t2 t) (pr0_comp t1 t2 H1
52 t t (pr0_refl t) k) (THead k t0 t) (subst0_fst u t0 t2 i H2 t k)))))))))))) c
56 \forall (c: C).(\forall (u: T).(\forall (t1: T).(\forall (t2: T).(\forall
57 (k: K).((pr2 (CHead c k u) t1 t2) \to (pr2 c (THead k u t1) (THead k u
60 \lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda
61 (k: K).(\lambda (H: (pr2 (CHead c k u) t1 t2)).(insert_eq C (CHead c k u)
62 (\lambda (c0: C).(pr2 c0 t1 t2)) (\lambda (_: C).(pr2 c (THead k u t1) (THead
63 k u t2))) (\lambda (y: C).(\lambda (H0: (pr2 y t1 t2)).(pr2_ind (\lambda (c0:
64 C).(\lambda (t: T).(\lambda (t0: T).((eq C c0 (CHead c k u)) \to (pr2 c
65 (THead k u t) (THead k u t0)))))) (\lambda (c0: C).(\lambda (t3: T).(\lambda
66 (t4: T).(\lambda (H1: (pr0 t3 t4)).(\lambda (_: (eq C c0 (CHead c k
67 u))).(pr2_free c (THead k u t3) (THead k u t4) (pr0_comp u u (pr0_refl u) t3
68 t4 H1 k))))))) (K_ind (\lambda (k0: K).(\forall (c0: C).(\forall (d:
69 C).(\forall (u0: T).(\forall (i: nat).((getl i c0 (CHead d (Bind Abbr) u0))
70 \to (\forall (t3: T).(\forall (t4: T).((pr0 t3 t4) \to (\forall (t:
71 T).((subst0 i u0 t4 t) \to ((eq C c0 (CHead c k0 u)) \to (pr2 c (THead k0 u
72 t3) (THead k0 u t)))))))))))))) (\lambda (b: B).(\lambda (c0: C).(\lambda (d:
73 C).(\lambda (u0: T).(\lambda (i: nat).(nat_ind (\lambda (n: nat).((getl n c0
74 (CHead d (Bind Abbr) u0)) \to (\forall (t3: T).(\forall (t4: T).((pr0 t3 t4)
75 \to (\forall (t: T).((subst0 n u0 t4 t) \to ((eq C c0 (CHead c (Bind b) u))
76 \to (pr2 c (THead (Bind b) u t3) (THead (Bind b) u t)))))))))) (\lambda (H1:
77 (getl O c0 (CHead d (Bind Abbr) u0))).(\lambda (t3: T).(\lambda (t4:
78 T).(\lambda (H2: (pr0 t3 t4)).(\lambda (t: T).(\lambda (H3: (subst0 O u0 t4
79 t)).(\lambda (H4: (eq C c0 (CHead c (Bind b) u))).(let H5 \def (eq_ind C c0
80 (\lambda (c1: C).(getl O c1 (CHead d (Bind Abbr) u0))) H1 (CHead c (Bind b)
81 u) H4) in (let H6 \def (f_equal C C (\lambda (e: C).(match e with [(CSort _)
82 \Rightarrow d | (CHead c1 _ _) \Rightarrow c1])) (CHead d (Bind Abbr) u0)
83 (CHead c (Bind b) u) (clear_gen_bind b c (CHead d (Bind Abbr) u0) u
84 (getl_gen_O (CHead c (Bind b) u) (CHead d (Bind Abbr) u0) H5))) in ((let H7
85 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _) \Rightarrow Abbr |
86 (CHead _ k0 _) \Rightarrow (match k0 with [(Bind b0) \Rightarrow b0 | (Flat
87 _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u0) (CHead c (Bind b) u)
88 (clear_gen_bind b c (CHead d (Bind Abbr) u0) u (getl_gen_O (CHead c (Bind b)
89 u) (CHead d (Bind Abbr) u0) H5))) in ((let H8 \def (f_equal C T (\lambda (e:
90 C).(match e with [(CSort _) \Rightarrow u0 | (CHead _ _ t0) \Rightarrow t0]))
91 (CHead d (Bind Abbr) u0) (CHead c (Bind b) u) (clear_gen_bind b c (CHead d
92 (Bind Abbr) u0) u (getl_gen_O (CHead c (Bind b) u) (CHead d (Bind Abbr) u0)
93 H5))) in (\lambda (H9: (eq B Abbr b)).(\lambda (_: (eq C d c)).(let H11 \def
94 (eq_ind T u0 (\lambda (t0: T).(subst0 O t0 t4 t)) H3 u H8) in (eq_ind B Abbr
95 (\lambda (b0: B).(pr2 c (THead (Bind b0) u t3) (THead (Bind b0) u t)))
96 (pr2_free c (THead (Bind Abbr) u t3) (THead (Bind Abbr) u t) (pr0_delta u u
97 (pr0_refl u) t3 t4 H2 t H11)) b H9))))) H7)) H6)))))))))) (\lambda (n:
98 nat).(\lambda (H1: (((getl n c0 (CHead d (Bind Abbr) u0)) \to (\forall (t3:
99 T).(\forall (t4: T).((pr0 t3 t4) \to (\forall (t: T).((subst0 n u0 t4 t) \to
100 ((eq C c0 (CHead c (Bind b) u)) \to (pr2 c (THead (Bind b) u t3) (THead (Bind
101 b) u t))))))))))).(\lambda (H2: (getl (S n) c0 (CHead d (Bind Abbr)
102 u0))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H3: (pr0 t3 t4)).(\lambda
103 (t: T).(\lambda (H4: (subst0 (S n) u0 t4 t)).(\lambda (H5: (eq C c0 (CHead c
104 (Bind b) u))).(let H6 \def (eq_ind C c0 (\lambda (c1: C).(getl (S n) c1
105 (CHead d (Bind Abbr) u0))) H2 (CHead c (Bind b) u) H5) in (let H7 \def
106 (eq_ind C c0 (\lambda (c1: C).((getl n c1 (CHead d (Bind Abbr) u0)) \to
107 (\forall (t5: T).(\forall (t6: T).((pr0 t5 t6) \to (\forall (t0: T).((subst0
108 n u0 t6 t0) \to ((eq C c1 (CHead c (Bind b) u)) \to (pr2 c (THead (Bind b) u
109 t5) (THead (Bind b) u t0)))))))))) H1 (CHead c (Bind b) u) H5) in (pr2_delta
110 c d u0 (r (Bind b) n) (getl_gen_S (Bind b) c (CHead d (Bind Abbr) u0) u n H6)
111 (THead (Bind b) u t3) (THead (Bind b) u t4) (pr0_comp u u (pr0_refl u) t3 t4
112 H3 (Bind b)) (THead (Bind b) u t) (subst0_snd (Bind b) u0 t t4 (r (Bind b) n)
113 H4 u))))))))))))) i)))))) (\lambda (f: F).(\lambda (c0: C).(\lambda (d:
114 C).(\lambda (u0: T).(\lambda (i: nat).(nat_ind (\lambda (n: nat).((getl n c0
115 (CHead d (Bind Abbr) u0)) \to (\forall (t3: T).(\forall (t4: T).((pr0 t3 t4)
116 \to (\forall (t: T).((subst0 n u0 t4 t) \to ((eq C c0 (CHead c (Flat f) u))
117 \to (pr2 c (THead (Flat f) u t3) (THead (Flat f) u t)))))))))) (\lambda (H1:
118 (getl O c0 (CHead d (Bind Abbr) u0))).(\lambda (t3: T).(\lambda (t4:
119 T).(\lambda (H2: (pr0 t3 t4)).(\lambda (t: T).(\lambda (H3: (subst0 O u0 t4
120 t)).(\lambda (H4: (eq C c0 (CHead c (Flat f) u))).(let H5 \def (eq_ind C c0
121 (\lambda (c1: C).(getl O c1 (CHead d (Bind Abbr) u0))) H1 (CHead c (Flat f)
122 u) H4) in (pr2_delta c d u0 O (getl_intro O c (CHead d (Bind Abbr) u0) c
123 (drop_refl c) (clear_gen_flat f c (CHead d (Bind Abbr) u0) u (getl_gen_O
124 (CHead c (Flat f) u) (CHead d (Bind Abbr) u0) H5))) (THead (Flat f) u t3)
125 (THead (Flat f) u t4) (pr0_comp u u (pr0_refl u) t3 t4 H2 (Flat f)) (THead
126 (Flat f) u t) (subst0_snd (Flat f) u0 t t4 O H3 u)))))))))) (\lambda (n:
127 nat).(\lambda (H1: (((getl n c0 (CHead d (Bind Abbr) u0)) \to (\forall (t3:
128 T).(\forall (t4: T).((pr0 t3 t4) \to (\forall (t: T).((subst0 n u0 t4 t) \to
129 ((eq C c0 (CHead c (Flat f) u)) \to (pr2 c (THead (Flat f) u t3) (THead (Flat
130 f) u t))))))))))).(\lambda (H2: (getl (S n) c0 (CHead d (Bind Abbr)
131 u0))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H3: (pr0 t3 t4)).(\lambda
132 (t: T).(\lambda (H4: (subst0 (S n) u0 t4 t)).(\lambda (H5: (eq C c0 (CHead c
133 (Flat f) u))).(let H6 \def (eq_ind C c0 (\lambda (c1: C).(getl (S n) c1
134 (CHead d (Bind Abbr) u0))) H2 (CHead c (Flat f) u) H5) in (let H7 \def
135 (eq_ind C c0 (\lambda (c1: C).((getl n c1 (CHead d (Bind Abbr) u0)) \to
136 (\forall (t5: T).(\forall (t6: T).((pr0 t5 t6) \to (\forall (t0: T).((subst0
137 n u0 t6 t0) \to ((eq C c1 (CHead c (Flat f) u)) \to (pr2 c (THead (Flat f) u
138 t5) (THead (Flat f) u t0)))))))))) H1 (CHead c (Flat f) u) H5) in (pr2_delta
139 c d u0 (r (Flat f) n) (getl_gen_S (Flat f) c (CHead d (Bind Abbr) u0) u n H6)
140 (THead (Flat f) u t3) (THead (Flat f) u t4) (pr0_comp u u (pr0_refl u) t3 t4
141 H3 (Flat f)) (THead (Flat f) u t) (subst0_snd (Flat f) u0 t t4 (r (Flat f) n)
142 H4 u))))))))))))) i)))))) k) y t1 t2 H0))) H)))))).
144 lemma clear_pr2_trans:
145 \forall (c2: C).(\forall (t1: T).(\forall (t2: T).((pr2 c2 t1 t2) \to
146 (\forall (c1: C).((clear c1 c2) \to (pr2 c1 t1 t2))))))
148 \lambda (c2: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c2 t1
149 t2)).(pr2_ind (\lambda (c: C).(\lambda (t: T).(\lambda (t0: T).(\forall (c1:
150 C).((clear c1 c) \to (pr2 c1 t t0)))))) (\lambda (c: C).(\lambda (t3:
151 T).(\lambda (t4: T).(\lambda (H0: (pr0 t3 t4)).(\lambda (c1: C).(\lambda (_:
152 (clear c1 c)).(pr2_free c1 t3 t4 H0))))))) (\lambda (c: C).(\lambda (d:
153 C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c (CHead d (Bind
154 Abbr) u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H1: (pr0 t3
155 t4)).(\lambda (t: T).(\lambda (H2: (subst0 i u t4 t)).(\lambda (c1:
156 C).(\lambda (H3: (clear c1 c)).(pr2_delta c1 d u i (clear_getl_trans i c
157 (CHead d (Bind Abbr) u) H0 c1 H3) t3 t4 H1 t H2))))))))))))) c2 t1 t2 H)))).
160 \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall
161 (f: F).(\forall (v: T).(pr2 (CHead c (Flat f) v) t1 t2))))))
163 \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t1
164 t2)).(\lambda (f: F).(\lambda (v: T).(pr2_ind (\lambda (c0: C).(\lambda (t:
165 T).(\lambda (t0: T).(pr2 (CHead c0 (Flat f) v) t t0)))) (\lambda (c0:
166 C).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H0: (pr0 t3 t4)).(pr2_free
167 (CHead c0 (Flat f) v) t3 t4 H0))))) (\lambda (c0: C).(\lambda (d: C).(\lambda
168 (u: T).(\lambda (i: nat).(\lambda (H0: (getl i c0 (CHead d (Bind Abbr)
169 u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H1: (pr0 t3 t4)).(\lambda
170 (t: T).(\lambda (H2: (subst0 i u t4 t)).(pr2_delta (CHead c0 (Flat f) v) d u
171 i (getl_flat c0 (CHead d (Bind Abbr) u) i H0 f v) t3 t4 H1 t H2))))))))))) c
175 \forall (c: C).(\forall (t1: T).(\forall (t2: T).((pr2 c t1 t2) \to (\forall
176 (k: K).(\forall (u: T).(pr2 (CTail k u c) t1 t2))))))
178 \lambda (c: C).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr2 c t1
179 t2)).(\lambda (k: K).(\lambda (u: T).(pr2_ind (\lambda (c0: C).(\lambda (t:
180 T).(\lambda (t0: T).(pr2 (CTail k u c0) t t0)))) (\lambda (c0: C).(\lambda
181 (t3: T).(\lambda (t4: T).(\lambda (H0: (pr0 t3 t4)).(pr2_free (CTail k u c0)
182 t3 t4 H0))))) (\lambda (c0: C).(\lambda (d: C).(\lambda (u0: T).(\lambda (i:
183 nat).(\lambda (H0: (getl i c0 (CHead d (Bind Abbr) u0))).(\lambda (t3:
184 T).(\lambda (t4: T).(\lambda (H1: (pr0 t3 t4)).(\lambda (t: T).(\lambda (H2:
185 (subst0 i u0 t4 t)).(pr2_delta (CTail k u c0) (CTail k u d) u0 i (getl_ctail
186 Abbr c0 d u0 i H0 k u) t3 t4 H1 t H2))))))))))) c t1 t2 H)))))).
189 \forall (b: B).((not (eq B b Abbr)) \to (\forall (c: C).(\forall (v1:
190 T).(\forall (t1: T).(\forall (t2: T).((pr2 (CHead c (Bind b) v1) t1 t2) \to
191 (\forall (v2: T).(pr2 (CHead c (Bind b) v2) t1 t2))))))))
193 \lambda (b: B).(\lambda (H: (not (eq B b Abbr))).(\lambda (c: C).(\lambda
194 (v1: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pr2 (CHead c (Bind
195 b) v1) t1 t2)).(\lambda (v2: T).(insert_eq C (CHead c (Bind b) v1) (\lambda
196 (c0: C).(pr2 c0 t1 t2)) (\lambda (_: C).(pr2 (CHead c (Bind b) v2) t1 t2))
197 (\lambda (y: C).(\lambda (H1: (pr2 y t1 t2)).(pr2_ind (\lambda (c0:
198 C).(\lambda (t: T).(\lambda (t0: T).((eq C c0 (CHead c (Bind b) v1)) \to (pr2
199 (CHead c (Bind b) v2) t t0))))) (\lambda (c0: C).(\lambda (t3: T).(\lambda
200 (t4: T).(\lambda (H2: (pr0 t3 t4)).(\lambda (_: (eq C c0 (CHead c (Bind b)
201 v1))).(pr2_free (CHead c (Bind b) v2) t3 t4 H2)))))) (\lambda (c0:
202 C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H2: (getl i c0
203 (CHead d (Bind Abbr) u))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H3:
204 (pr0 t3 t4)).(\lambda (t: T).(\lambda (H4: (subst0 i u t4 t)).(\lambda (H5:
205 (eq C c0 (CHead c (Bind b) v1))).(let H6 \def (eq_ind C c0 (\lambda (c1:
206 C).(getl i c1 (CHead d (Bind Abbr) u))) H2 (CHead c (Bind b) v1) H5) in
207 (nat_ind (\lambda (n: nat).((getl n (CHead c (Bind b) v1) (CHead d (Bind
208 Abbr) u)) \to ((subst0 n u t4 t) \to (pr2 (CHead c (Bind b) v2) t3 t))))
209 (\lambda (H7: (getl O (CHead c (Bind b) v1) (CHead d (Bind Abbr)
210 u))).(\lambda (H8: (subst0 O u t4 t)).(let H9 \def (f_equal C C (\lambda (e:
211 C).(match e with [(CSort _) \Rightarrow d | (CHead c1 _ _) \Rightarrow c1]))
212 (CHead d (Bind Abbr) u) (CHead c (Bind b) v1) (clear_gen_bind b c (CHead d
213 (Bind Abbr) u) v1 (getl_gen_O (CHead c (Bind b) v1) (CHead d (Bind Abbr) u)
214 H7))) in ((let H10 \def (f_equal C B (\lambda (e: C).(match e with [(CSort _)
215 \Rightarrow Abbr | (CHead _ k _) \Rightarrow (match k with [(Bind b0)
216 \Rightarrow b0 | (Flat _) \Rightarrow Abbr])])) (CHead d (Bind Abbr) u)
217 (CHead c (Bind b) v1) (clear_gen_bind b c (CHead d (Bind Abbr) u) v1
218 (getl_gen_O (CHead c (Bind b) v1) (CHead d (Bind Abbr) u) H7))) in ((let H11
219 \def (f_equal C T (\lambda (e: C).(match e with [(CSort _) \Rightarrow u |
220 (CHead _ _ t0) \Rightarrow t0])) (CHead d (Bind Abbr) u) (CHead c (Bind b)
221 v1) (clear_gen_bind b c (CHead d (Bind Abbr) u) v1 (getl_gen_O (CHead c (Bind
222 b) v1) (CHead d (Bind Abbr) u) H7))) in (\lambda (H12: (eq B Abbr
223 b)).(\lambda (_: (eq C d c)).(let H14 \def (eq_ind T u (\lambda (t0:
224 T).(subst0 O t0 t4 t)) H8 v1 H11) in (let H15 \def (eq_ind_r B b (\lambda
225 (b0: B).(not (eq B b0 Abbr))) H Abbr H12) in (eq_ind B Abbr (\lambda (b0:
226 B).(pr2 (CHead c (Bind b0) v2) t3 t)) (let H16 \def (match (H15 (refl_equal B
227 Abbr)) in False with []) in H16) b H12)))))) H10)) H9)))) (\lambda (i0:
228 nat).(\lambda (_: (((getl i0 (CHead c (Bind b) v1) (CHead d (Bind Abbr) u))
229 \to ((subst0 i0 u t4 t) \to (pr2 (CHead c (Bind b) v2) t3 t))))).(\lambda
230 (H7: (getl (S i0) (CHead c (Bind b) v1) (CHead d (Bind Abbr) u))).(\lambda
231 (H8: (subst0 (S i0) u t4 t)).(pr2_delta (CHead c (Bind b) v2) d u (S i0)
232 (getl_head (Bind b) i0 c (CHead d (Bind Abbr) u) (getl_gen_S (Bind b) c
233 (CHead d (Bind Abbr) u) v1 i0 H7) v2) t3 t4 H3 t H8))))) i H6 H4)))))))))))))
234 y t1 t2 H1))) H0)))))))).
237 \forall (c: C).(\forall (e: C).(\forall (h: nat).(\forall (d: nat).((drop h
238 d c e) \to (\forall (t1: T).(\forall (t2: T).((pr2 e t1 t2) \to (pr2 c (lift
239 h d t1) (lift h d t2)))))))))
241 \lambda (c: C).(\lambda (e: C).(\lambda (h: nat).(\lambda (d: nat).(\lambda
242 (H: (drop h d c e)).(\lambda (t1: T).(\lambda (t2: T).(\lambda (H0: (pr2 e t1
243 t2)).(insert_eq C e (\lambda (c0: C).(pr2 c0 t1 t2)) (\lambda (_: C).(pr2 c
244 (lift h d t1) (lift h d t2))) (\lambda (y: C).(\lambda (H1: (pr2 y t1
245 t2)).(pr2_ind (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).((eq C c0 e)
246 \to (pr2 c (lift h d t) (lift h d t0)))))) (\lambda (c0: C).(\lambda (t3:
247 T).(\lambda (t4: T).(\lambda (H2: (pr0 t3 t4)).(\lambda (_: (eq C c0
248 e)).(pr2_free c (lift h d t3) (lift h d t4) (pr0_lift t3 t4 H2 h d)))))))
249 (\lambda (c0: C).(\lambda (d0: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
250 (H2: (getl i c0 (CHead d0 (Bind Abbr) u))).(\lambda (t3: T).(\lambda (t4:
251 T).(\lambda (H3: (pr0 t3 t4)).(\lambda (t: T).(\lambda (H4: (subst0 i u t4
252 t)).(\lambda (H5: (eq C c0 e)).(let H6 \def (eq_ind C c0 (\lambda (c1:
253 C).(getl i c1 (CHead d0 (Bind Abbr) u))) H2 e H5) in (lt_le_e i d (pr2 c
254 (lift h d t3) (lift h d t)) (\lambda (H7: (lt i d)).(let H8 \def
255 (drop_getl_trans_le i d (le_S_n i d (le_S_n (S i) (S d) (le_S (S (S i)) (S d)
256 (le_n_S (S i) d H7)))) c e h H (CHead d0 (Bind Abbr) u) H6) in (ex3_2_ind C C
257 (\lambda (e0: C).(\lambda (_: C).(drop i O c e0))) (\lambda (e0: C).(\lambda
258 (e1: C).(drop h (minus d i) e0 e1))) (\lambda (_: C).(\lambda (e1: C).(clear
259 e1 (CHead d0 (Bind Abbr) u)))) (pr2 c (lift h d t3) (lift h d t)) (\lambda
260 (x0: C).(\lambda (x1: C).(\lambda (H9: (drop i O c x0)).(\lambda (H10: (drop
261 h (minus d i) x0 x1)).(\lambda (H11: (clear x1 (CHead d0 (Bind Abbr)
262 u))).(let H12 \def (eq_ind nat (minus d i) (\lambda (n: nat).(drop h n x0
263 x1)) H10 (S (minus d (S i))) (minus_x_Sy d i H7)) in (let H13 \def
264 (drop_clear_S x1 x0 h (minus d (S i)) H12 Abbr d0 u H11) in (ex2_ind C
265 (\lambda (c1: C).(clear x0 (CHead c1 (Bind Abbr) (lift h (minus d (S i))
266 u)))) (\lambda (c1: C).(drop h (minus d (S i)) c1 d0)) (pr2 c (lift h d t3)
267 (lift h d t)) (\lambda (x: C).(\lambda (H14: (clear x0 (CHead x (Bind Abbr)
268 (lift h (minus d (S i)) u)))).(\lambda (_: (drop h (minus d (S i)) x
269 d0)).(pr2_delta c x (lift h (minus d (S i)) u) i (getl_intro i c (CHead x
270 (Bind Abbr) (lift h (minus d (S i)) u)) x0 H9 H14) (lift h d t3) (lift h d
271 t4) (pr0_lift t3 t4 H3 h d) (lift h d t) (subst0_lift_lt t4 t u i H4 d H7
272 h))))) H13)))))))) H8))) (\lambda (H7: (le d i)).(pr2_delta c d0 u (plus i h)
273 (drop_getl_trans_ge i c e d h H (CHead d0 (Bind Abbr) u) H6 H7) (lift h d t3)
274 (lift h d t4) (pr0_lift t3 t4 H3 h d) (lift h d t) (subst0_lift_ge t4 t u i h
275 H4 d H7)))))))))))))))) y t1 t2 H1))) H0)))))))).
278 \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c
279 (THead (Bind Abbr) u1 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda
280 (t2: T).(eq T x (THead (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_:
281 T).(pr2 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(or3 (\forall (b:
282 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) t1 t2))) (ex2 T (\lambda (u:
283 T).(pr0 u1 u)) (\lambda (u: T).(pr2 (CHead c (Bind Abbr) u) t1 t2))) (ex3_2 T
284 T (\lambda (y: T).(\lambda (_: T).(pr2 (CHead c (Bind Abbr) u1) t1 y)))
285 (\lambda (y: T).(\lambda (z: T).(pr0 y z))) (\lambda (_: T).(\lambda (z:
286 T).(pr2 (CHead c (Bind Abbr) u1) z t2)))))))) (\forall (b: B).(\forall (u:
287 T).(pr2 (CHead c (Bind b) u) t1 (lift (S O) O x)))))))))
289 \lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda
290 (H: (pr2 c (THead (Bind Abbr) u1 t1) x)).(insert_eq T (THead (Bind Abbr) u1
291 t1) (\lambda (t: T).(pr2 c t x)) (\lambda (_: T).(or (ex3_2 T T (\lambda (u2:
292 T).(\lambda (t2: T).(eq T x (THead (Bind Abbr) u2 t2)))) (\lambda (u2:
293 T).(\lambda (_: T).(pr2 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(or3
294 (\forall (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) t1 t2))) (ex2 T
295 (\lambda (u: T).(pr0 u1 u)) (\lambda (u: T).(pr2 (CHead c (Bind Abbr) u) t1
296 t2))) (ex3_2 T T (\lambda (y: T).(\lambda (_: T).(pr2 (CHead c (Bind Abbr)
297 u1) t1 y))) (\lambda (y: T).(\lambda (z: T).(pr0 y z))) (\lambda (_:
298 T).(\lambda (z: T).(pr2 (CHead c (Bind Abbr) u1) z t2)))))))) (\forall (b:
299 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) t1 (lift (S O) O x))))))
300 (\lambda (y: T).(\lambda (H0: (pr2 c y x)).(pr2_ind (\lambda (c0: C).(\lambda
301 (t: T).(\lambda (t0: T).((eq T t (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T
302 T (\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Bind Abbr) u2 t2))))
303 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
304 (t2: T).(or3 (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1
305 t2))) (ex2 T (\lambda (u: T).(pr0 u1 u)) (\lambda (u: T).(pr2 (CHead c0 (Bind
306 Abbr) u) t1 t2))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0
307 (Bind Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z)))
308 (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t2))))))))
309 (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O
310 t0))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H1:
311 (pr0 t0 t2)).(\lambda (H2: (eq T t0 (THead (Bind Abbr) u1 t1))).(let H3 \def
312 (eq_ind T t0 (\lambda (t: T).(pr0 t t2)) H1 (THead (Bind Abbr) u1 t1) H2) in
313 (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
314 Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2:
315 T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
316 (\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S O) O t2)) (or
317 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2
318 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_:
319 T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind
320 b) u) t1 t3))) (ex2 T (\lambda (u: T).(pr0 u1 u)) (\lambda (u: T).(pr2 (CHead
321 c0 (Bind Abbr) u) t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2
322 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0
323 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z
324 t3)))))))) (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1
325 (lift (S O) O t2))))) (\lambda (H4: (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
326 T).(eq T t2 (THead (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_:
327 T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T
328 (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0
329 t3)))))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead
330 (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda
331 (u2: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
332 (\lambda (y0: T).(subst0 O u2 y0 t3)))))) (or (ex3_2 T T (\lambda (u2:
333 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
334 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3
335 (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1 t3))) (ex2 T
336 (\lambda (u: T).(pr0 u1 u)) (\lambda (u: T).(pr2 (CHead c0 (Bind Abbr) u) t1
337 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr)
338 u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_:
339 T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3)))))))) (\forall (b:
340 B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2)))))
341 (\lambda (x0: T).(\lambda (x1: T).(\lambda (H5: (eq T t2 (THead (Bind Abbr)
342 x0 x1))).(\lambda (H6: (pr0 u1 x0)).(\lambda (H_x: (or (pr0 t1 x1) (ex2 T
343 (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O x0 y0
344 x1))))).(or_ind (pr0 t1 x1) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda
345 (y0: T).(subst0 O x0 y0 x1))) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
346 T).(eq T t2 (THead (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_:
347 T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b:
348 B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1 t3))) (ex2 T (\lambda (u:
349 T).(pr0 u1 u)) (\lambda (u: T).(pr2 (CHead c0 (Bind Abbr) u) t1 t3))) (ex3_2
350 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0)))
351 (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z:
352 T).(pr2 (CHead c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u:
353 T).(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))))) (\lambda (H7: (pr0 t1
354 x1)).(eq_ind_r T (THead (Bind Abbr) x0 x1) (\lambda (t: T).(or (ex3_2 T T
355 (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3))))
356 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
357 (t3: T).(or3 (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1
358 t3))) (ex2 T (\lambda (u: T).(pr0 u1 u)) (\lambda (u: T).(pr2 (CHead c0 (Bind
359 Abbr) u) t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0
360 (Bind Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z)))
361 (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3))))))))
362 (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O
363 t)))))) (or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T (THead
364 (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_:
365 T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b:
366 B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1 t3))) (ex2 T (\lambda (u:
367 T).(pr0 u1 u)) (\lambda (u: T).(pr2 (CHead c0 (Bind Abbr) u) t1 t3))) (ex3_2
368 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0)))
369 (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z:
370 T).(pr2 (CHead c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u:
371 T).(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O (THead (Bind Abbr) x0 x1)))))
372 (ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr)
373 x0 x1) (THead (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0
374 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u:
375 T).(pr2 (CHead c0 (Bind b) u) t1 t3))) (ex2 T (\lambda (u: T).(pr0 u1 u))
376 (\lambda (u: T).(pr2 (CHead c0 (Bind Abbr) u) t1 t3))) (ex3_2 T T (\lambda
377 (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
378 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
379 c0 (Bind Abbr) u1) z t3))))))) x0 x1 (refl_equal T (THead (Bind Abbr) x0 x1))
380 (pr2_free c0 u1 x0 H6) (or3_intro0 (\forall (b: B).(\forall (u: T).(pr2
381 (CHead c0 (Bind b) u) t1 x1))) (ex2 T (\lambda (u: T).(pr0 u1 u)) (\lambda
382 (u: T).(pr2 (CHead c0 (Bind Abbr) u) t1 x1))) (ex3_2 T T (\lambda (y0:
383 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
384 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
385 c0 (Bind Abbr) u1) z x1)))) (\lambda (b: B).(\lambda (u: T).(pr2_free (CHead
386 c0 (Bind b) u) t1 x1 H7)))))) t2 H5)) (\lambda (H_x0: (ex2 T (\lambda (y0:
387 T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O x0 y0 x1)))).(ex2_ind T (\lambda
388 (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O x0 y0 x1)) (or (ex3_2 T T
389 (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3))))
390 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
391 (t3: T).(or3 (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1
392 t3))) (ex2 T (\lambda (u: T).(pr0 u1 u)) (\lambda (u: T).(pr2 (CHead c0 (Bind
393 Abbr) u) t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0
394 (Bind Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z)))
395 (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3))))))))
396 (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O
397 t2))))) (\lambda (x2: T).(\lambda (H7: (pr0 t1 x2)).(\lambda (H8: (subst0 O
398 x0 x2 x1)).(eq_ind_r T (THead (Bind Abbr) x0 x1) (\lambda (t: T).(or (ex3_2 T
399 T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3))))
400 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
401 (t3: T).(or3 (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1
402 t3))) (ex2 T (\lambda (u: T).(pr0 u1 u)) (\lambda (u: T).(pr2 (CHead c0 (Bind
403 Abbr) u) t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0
404 (Bind Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z)))
405 (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3))))))))
406 (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O
407 t)))))) (ex2_ind T (\lambda (t: T).(subst0 O u1 x2 t)) (\lambda (t: T).(pr0 t
408 x1)) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T (THead (Bind
409 Abbr) x0 x1) (THead (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_:
410 T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b:
411 B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1 t3))) (ex2 T (\lambda (u:
412 T).(pr0 u1 u)) (\lambda (u: T).(pr2 (CHead c0 (Bind Abbr) u) t1 t3))) (ex3_2
413 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0)))
414 (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z:
415 T).(pr2 (CHead c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u:
416 T).(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O (THead (Bind Abbr) x0 x1))))))
417 (\lambda (x3: T).(\lambda (_: (subst0 O u1 x2 x3)).(\lambda (_: (pr0 x3
418 x1)).(or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T (THead
419 (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_:
420 T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b:
421 B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1 t3))) (ex2 T (\lambda (u:
422 T).(pr0 u1 u)) (\lambda (u: T).(pr2 (CHead c0 (Bind Abbr) u) t1 t3))) (ex3_2
423 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0)))
424 (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z:
425 T).(pr2 (CHead c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u:
426 T).(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O (THead (Bind Abbr) x0 x1)))))
427 (ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr)
428 x0 x1) (THead (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0
429 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u:
430 T).(pr2 (CHead c0 (Bind b) u) t1 t3))) (ex2 T (\lambda (u: T).(pr0 u1 u))
431 (\lambda (u: T).(pr2 (CHead c0 (Bind Abbr) u) t1 t3))) (ex3_2 T T (\lambda
432 (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
433 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
434 c0 (Bind Abbr) u1) z t3))))))) x0 x1 (refl_equal T (THead (Bind Abbr) x0 x1))
435 (pr2_free c0 u1 x0 H6) (or3_intro1 (\forall (b: B).(\forall (u: T).(pr2
436 (CHead c0 (Bind b) u) t1 x1))) (ex2 T (\lambda (u: T).(pr0 u1 u)) (\lambda
437 (u: T).(pr2 (CHead c0 (Bind Abbr) u) t1 x1))) (ex3_2 T T (\lambda (y0:
438 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
439 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
440 c0 (Bind Abbr) u1) z x1)))) (ex_intro2 T (\lambda (u: T).(pr0 u1 u)) (\lambda
441 (u: T).(pr2 (CHead c0 (Bind Abbr) u) t1 x1)) x0 H6 (pr2_delta (CHead c0 (Bind
442 Abbr) x0) c0 x0 O (getl_refl Abbr c0 x0) t1 x2 H7 x1 H8))))))))
443 (pr0_subst0_back x0 x2 x1 O H8 u1 H6)) t2 H5)))) H_x0)) H_x)))))) H4))
444 (\lambda (H4: (pr0 t1 (lift (S O) O t2))).(or_intror (ex3_2 T T (\lambda (u2:
445 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
446 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3
447 (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1 t3))) (ex2 T
448 (\lambda (u: T).(pr0 u1 u)) (\lambda (u: T).(pr2 (CHead c0 (Bind Abbr) u) t1
449 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr)
450 u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_:
451 T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3)))))))) (\forall (b:
452 B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1 (lift (S O) O t2))))
453 (\lambda (b: B).(\lambda (u: T).(pr2_free (CHead c0 (Bind b) u) t1 (lift (S
454 O) O t2) H4))))) (pr0_gen_abbr u1 t1 t2 H3)))))))) (\lambda (c0: C).(\lambda
455 (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda (H1: (getl i c0 (CHead d
456 (Bind Abbr) u))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H2: (pr0 t0
457 t2)).(\lambda (t: T).(\lambda (H3: (subst0 i u t2 t)).(\lambda (H4: (eq T t0
458 (THead (Bind Abbr) u1 t1))).(let H5 \def (eq_ind T t0 (\lambda (t3: T).(pr0
459 t3 t2)) H2 (THead (Bind Abbr) u1 t1) H4) in (or_ind (ex3_2 T T (\lambda (u2:
460 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
461 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t3: T).(or (pr0
462 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0
463 t3))))))) (pr0 t1 (lift (S O) O t2)) (or (ex3_2 T T (\lambda (u2: T).(\lambda
464 (t3: T).(eq T t (THead (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_:
465 T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b:
466 B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T (\lambda (u0:
467 T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0) t1 t3)))
468 (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1
469 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda
470 (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall
471 (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))))) (\lambda (H6:
472 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2
473 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2:
474 T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
475 (\lambda (y0: T).(subst0 O u2 y0 t3)))))))).(ex3_2_ind T T (\lambda (u2:
476 T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
477 T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t3: T).(or (pr0
478 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0
479 t3)))))) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead
480 (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2)))
481 (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2
482 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda
483 (u0: T).(pr2 (CHead c0 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0:
484 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
485 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
486 c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead
487 c0 (Bind b) u0) t1 (lift (S O) O t))))) (\lambda (x0: T).(\lambda (x1:
488 T).(\lambda (H7: (eq T t2 (THead (Bind Abbr) x0 x1))).(\lambda (H8: (pr0 u1
489 x0)).(\lambda (H_x: (or (pr0 t1 x1) (ex2 T (\lambda (y0: T).(pr0 t1 y0))
490 (\lambda (y0: T).(subst0 O x0 y0 x1))))).(or_ind (pr0 t1 x1) (ex2 T (\lambda
491 (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O x0 y0 x1))) (or (ex3_2 T T
492 (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3))))
493 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
494 (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
495 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0
496 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2
497 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0
498 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z
499 t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
500 (lift (S O) O t))))) (\lambda (H9: (pr0 t1 x1)).(let H10 \def (eq_ind T t2
501 (\lambda (t3: T).(subst0 i u t3 t)) H3 (THead (Bind Abbr) x0 x1) H7) in
502 (or3_ind (ex2 T (\lambda (u2: T).(eq T t (THead (Bind Abbr) u2 x1))) (\lambda
503 (u2: T).(subst0 i u x0 u2))) (ex2 T (\lambda (t3: T).(eq T t (THead (Bind
504 Abbr) x0 t3))) (\lambda (t3: T).(subst0 (s (Bind Abbr) i) u x1 t3))) (ex3_2 T
505 T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3))))
506 (\lambda (u2: T).(\lambda (_: T).(subst0 i u x0 u2))) (\lambda (_:
507 T).(\lambda (t3: T).(subst0 (s (Bind Abbr) i) u x1 t3)))) (or (ex3_2 T T
508 (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3))))
509 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
510 (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
511 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0
512 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2
513 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0
514 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z
515 t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
516 (lift (S O) O t))))) (\lambda (H11: (ex2 T (\lambda (u2: T).(eq T t (THead
517 (Bind Abbr) u2 x1))) (\lambda (u2: T).(subst0 i u x0 u2)))).(ex2_ind T
518 (\lambda (u2: T).(eq T t (THead (Bind Abbr) u2 x1))) (\lambda (u2: T).(subst0
519 i u x0 u2)) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead
520 (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2)))
521 (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2
522 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda
523 (u0: T).(pr2 (CHead c0 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0:
524 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
525 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
526 c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead
527 c0 (Bind b) u0) t1 (lift (S O) O t))))) (\lambda (x2: T).(\lambda (H12: (eq T
528 t (THead (Bind Abbr) x2 x1))).(\lambda (H13: (subst0 i u x0 x2)).(or_introl
529 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2
530 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_:
531 T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0
532 (Bind b) u0) t1 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0:
533 T).(pr2 (CHead c0 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0:
534 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
535 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
536 c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead
537 c0 (Bind b) u0) t1 (lift (S O) O t)))) (ex3_2_intro T T (\lambda (u2:
538 T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
539 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3
540 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T
541 (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0)
542 t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind
543 Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_:
544 T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3))))))) x2 x1 H12
545 (pr2_delta c0 d u i H1 u1 x0 H8 x2 H13) (or3_intro0 (\forall (b: B).(\forall
546 (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 x1))) (ex2 T (\lambda (u0: T).(pr0 u1
547 u0)) (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0) t1 x1))) (ex3_2 T T
548 (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0)))
549 (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z:
550 T).(pr2 (CHead c0 (Bind Abbr) u1) z x1)))) (\lambda (b: B).(\lambda (u0:
551 T).(pr2_free (CHead c0 (Bind b) u0) t1 x1 H9))))))))) H11)) (\lambda (H11:
552 (ex2 T (\lambda (t3: T).(eq T t (THead (Bind Abbr) x0 t3))) (\lambda (t3:
553 T).(subst0 (s (Bind Abbr) i) u x1 t3)))).(ex2_ind T (\lambda (t3: T).(eq T t
554 (THead (Bind Abbr) x0 t3))) (\lambda (t3: T).(subst0 (s (Bind Abbr) i) u x1
555 t3)) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind
556 Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda
557 (_: T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0
558 (Bind b) u0) t1 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0:
559 T).(pr2 (CHead c0 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0:
560 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
561 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
562 c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead
563 c0 (Bind b) u0) t1 (lift (S O) O t))))) (\lambda (x2: T).(\lambda (H12: (eq T
564 t (THead (Bind Abbr) x0 x2))).(\lambda (H13: (subst0 (s (Bind Abbr) i) u x1
565 x2)).(or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead
566 (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2)))
567 (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2
568 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda
569 (u0: T).(pr2 (CHead c0 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0:
570 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
571 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
572 c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead
573 c0 (Bind b) u0) t1 (lift (S O) O t)))) (ex3_2_intro T T (\lambda (u2:
574 T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
575 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3
576 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T
577 (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0)
578 t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind
579 Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_:
580 T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3))))))) x0 x2 H12
581 (pr2_free c0 u1 x0 H8) (or3_intro0 (\forall (b: B).(\forall (u0: T).(pr2
582 (CHead c0 (Bind b) u0) t1 x2))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda
583 (u0: T).(pr2 (CHead c0 (Bind Abbr) u0) t1 x2))) (ex3_2 T T (\lambda (y0:
584 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
585 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
586 c0 (Bind Abbr) u1) z x2)))) (\lambda (b: B).(\lambda (u0: T).(pr2_delta
587 (CHead c0 (Bind b) u0) d u (S i) (getl_head (Bind b) i c0 (CHead d (Bind
588 Abbr) u) H1 u0) t1 x1 H9 x2 H13))))))))) H11)) (\lambda (H11: (ex3_2 T T
589 (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3))))
590 (\lambda (u2: T).(\lambda (_: T).(subst0 i u x0 u2))) (\lambda (_:
591 T).(\lambda (t3: T).(subst0 (s (Bind Abbr) i) u x1 t3))))).(ex3_2_ind T T
592 (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3))))
593 (\lambda (u2: T).(\lambda (_: T).(subst0 i u x0 u2))) (\lambda (_:
594 T).(\lambda (t3: T).(subst0 (s (Bind Abbr) i) u x1 t3))) (or (ex3_2 T T
595 (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3))))
596 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
597 (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
598 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0
599 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2
600 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0
601 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z
602 t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
603 (lift (S O) O t))))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H12: (eq T t
604 (THead (Bind Abbr) x2 x3))).(\lambda (H13: (subst0 i u x0 x2)).(\lambda (H14:
605 (subst0 (s (Bind Abbr) i) u x1 x3)).(or_introl (ex3_2 T T (\lambda (u2:
606 T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
607 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3
608 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T
609 (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0)
610 t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind
611 Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_:
612 T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3)))))))) (\forall (b:
613 B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))))
614 (ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr)
615 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_:
616 T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0
617 (Bind b) u0) t1 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0:
618 T).(pr2 (CHead c0 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0:
619 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
620 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
621 c0 (Bind Abbr) u1) z t3))))))) x2 x3 H12 (pr2_delta c0 d u i H1 u1 x0 H8 x2
622 H13) (or3_intro0 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0)
623 t1 x3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0
624 (Bind Abbr) u0) t1 x3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2
625 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0
626 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z x3))))
627 (\lambda (b: B).(\lambda (u0: T).(pr2_delta (CHead c0 (Bind b) u0) d u (S i)
628 (getl_head (Bind b) i c0 (CHead d (Bind Abbr) u) H1 u0) t1 x1 H9 x3
629 H14))))))))))) H11)) (subst0_gen_head (Bind Abbr) u x0 x1 t i H10))))
630 (\lambda (H_x0: (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0
631 O x0 y0 x1)))).(ex2_ind T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0:
632 T).(subst0 O x0 y0 x1)) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq
633 T t (THead (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1
634 u2))) (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u0:
635 T).(pr2 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0))
636 (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda
637 (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
638 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
639 c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead
640 c0 (Bind b) u0) t1 (lift (S O) O t))))) (\lambda (x2: T).(\lambda (H9: (pr0
641 t1 x2)).(\lambda (H10: (subst0 O x0 x2 x1)).(let H11 \def (eq_ind T t2
642 (\lambda (t3: T).(subst0 i u t3 t)) H3 (THead (Bind Abbr) x0 x1) H7) in
643 (or3_ind (ex2 T (\lambda (u2: T).(eq T t (THead (Bind Abbr) u2 x1))) (\lambda
644 (u2: T).(subst0 i u x0 u2))) (ex2 T (\lambda (t3: T).(eq T t (THead (Bind
645 Abbr) x0 t3))) (\lambda (t3: T).(subst0 (s (Bind Abbr) i) u x1 t3))) (ex3_2 T
646 T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3))))
647 (\lambda (u2: T).(\lambda (_: T).(subst0 i u x0 u2))) (\lambda (_:
648 T).(\lambda (t3: T).(subst0 (s (Bind Abbr) i) u x1 t3)))) (or (ex3_2 T T
649 (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3))))
650 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
651 (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
652 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0
653 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2
654 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0
655 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z
656 t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
657 (lift (S O) O t))))) (\lambda (H12: (ex2 T (\lambda (u2: T).(eq T t (THead
658 (Bind Abbr) u2 x1))) (\lambda (u2: T).(subst0 i u x0 u2)))).(ex2_ind T
659 (\lambda (u2: T).(eq T t (THead (Bind Abbr) u2 x1))) (\lambda (u2: T).(subst0
660 i u x0 u2)) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead
661 (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2)))
662 (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2
663 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda
664 (u0: T).(pr2 (CHead c0 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0:
665 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
666 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
667 c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead
668 c0 (Bind b) u0) t1 (lift (S O) O t))))) (\lambda (x3: T).(\lambda (H13: (eq T
669 t (THead (Bind Abbr) x3 x1))).(\lambda (H14: (subst0 i u x0 x3)).(ex2_ind T
670 (\lambda (t3: T).(subst0 O u1 x2 t3)) (\lambda (t3: T).(pr0 t3 x1)) (or
671 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2
672 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_:
673 T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0
674 (Bind b) u0) t1 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0:
675 T).(pr2 (CHead c0 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0:
676 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
677 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
678 c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead
679 c0 (Bind b) u0) t1 (lift (S O) O t))))) (\lambda (x4: T).(\lambda (_: (subst0
680 O u1 x2 x4)).(\lambda (_: (pr0 x4 x1)).(or_introl (ex3_2 T T (\lambda (u2:
681 T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
682 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3
683 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T
684 (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0)
685 t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind
686 Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_:
687 T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3)))))))) (\forall (b:
688 B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))))
689 (ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr)
690 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_:
691 T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0
692 (Bind b) u0) t1 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0:
693 T).(pr2 (CHead c0 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0:
694 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
695 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
696 c0 (Bind Abbr) u1) z t3))))))) x3 x1 H13 (pr2_delta c0 d u i H1 u1 x0 H8 x3
697 H14) (or3_intro1 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0)
698 t1 x1))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0
699 (Bind Abbr) u0) t1 x1))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2
700 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0
701 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z x1))))
702 (ex_intro2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0
703 (Bind Abbr) u0) t1 x1)) x0 H8 (pr2_delta (CHead c0 (Bind Abbr) x0) c0 x0 O
704 (getl_refl Abbr c0 x0) t1 x2 H9 x1 H10)))))))) (pr0_subst0_back x0 x2 x1 O
705 H10 u1 H8))))) H12)) (\lambda (H12: (ex2 T (\lambda (t3: T).(eq T t (THead
706 (Bind Abbr) x0 t3))) (\lambda (t3: T).(subst0 (s (Bind Abbr) i) u x1
707 t3)))).(ex2_ind T (\lambda (t3: T).(eq T t (THead (Bind Abbr) x0 t3)))
708 (\lambda (t3: T).(subst0 (s (Bind Abbr) i) u x1 t3)) (or (ex3_2 T T (\lambda
709 (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
710 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3
711 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T
712 (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0)
713 t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind
714 Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_:
715 T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3)))))))) (\forall (b:
716 B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t)))))
717 (\lambda (x3: T).(\lambda (H13: (eq T t (THead (Bind Abbr) x0 x3))).(\lambda
718 (H14: (subst0 (s (Bind Abbr) i) u x1 x3)).(ex2_ind T (\lambda (t3: T).(subst0
719 O u1 x2 t3)) (\lambda (t3: T).(pr0 t3 x1)) (or (ex3_2 T T (\lambda (u2:
720 T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
721 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3
722 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T
723 (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0)
724 t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind
725 Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_:
726 T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3)))))))) (\forall (b:
727 B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t)))))
728 (\lambda (x4: T).(\lambda (H15: (subst0 O u1 x2 x4)).(\lambda (H16: (pr0 x4
729 x1)).(or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead
730 (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2)))
731 (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2
732 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda
733 (u0: T).(pr2 (CHead c0 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0:
734 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
735 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
736 c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead
737 c0 (Bind b) u0) t1 (lift (S O) O t)))) (ex3_2_intro T T (\lambda (u2:
738 T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
739 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3
740 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T
741 (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0)
742 t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind
743 Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_:
744 T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3))))))) x0 x3 H13
745 (pr2_free c0 u1 x0 H8) (or3_intro2 (\forall (b: B).(\forall (u0: T).(pr2
746 (CHead c0 (Bind b) u0) t1 x3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda
747 (u0: T).(pr2 (CHead c0 (Bind Abbr) u0) t1 x3))) (ex3_2 T T (\lambda (y0:
748 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
749 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
750 c0 (Bind Abbr) u1) z x3)))) (ex3_2_intro T T (\lambda (y0: T).(\lambda (_:
751 T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z:
752 T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr)
753 u1) z x3))) x4 x1 (pr2_delta (CHead c0 (Bind Abbr) u1) c0 u1 O (getl_refl
754 Abbr c0 u1) t1 x2 H9 x4 H15) H16 (pr2_delta (CHead c0 (Bind Abbr) u1) d u (S
755 i) (getl_head (Bind Abbr) i c0 (CHead d (Bind Abbr) u) H1 u1) x1 x1 (pr0_refl
756 x1) x3 H14)))))))) (pr0_subst0_back x0 x2 x1 O H10 u1 H8))))) H12)) (\lambda
757 (H12: (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr)
758 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u x0 u2))) (\lambda (_:
759 T).(\lambda (t3: T).(subst0 (s (Bind Abbr) i) u x1 t3))))).(ex3_2_ind T T
760 (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3))))
761 (\lambda (u2: T).(\lambda (_: T).(subst0 i u x0 u2))) (\lambda (_:
762 T).(\lambda (t3: T).(subst0 (s (Bind Abbr) i) u x1 t3))) (or (ex3_2 T T
763 (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3))))
764 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
765 (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
766 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0
767 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2
768 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0
769 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z
770 t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
771 (lift (S O) O t))))) (\lambda (x3: T).(\lambda (x4: T).(\lambda (H13: (eq T t
772 (THead (Bind Abbr) x3 x4))).(\lambda (H14: (subst0 i u x0 x3)).(\lambda (H15:
773 (subst0 (s (Bind Abbr) i) u x1 x4)).(ex2_ind T (\lambda (t3: T).(subst0 O u1
774 x2 t3)) (\lambda (t3: T).(pr0 t3 x1)) (or (ex3_2 T T (\lambda (u2:
775 T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
776 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3
777 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T
778 (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0)
779 t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind
780 Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_:
781 T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3)))))))) (\forall (b:
782 B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t)))))
783 (\lambda (x5: T).(\lambda (H16: (subst0 O u1 x2 x5)).(\lambda (H17: (pr0 x5
784 x1)).(or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead
785 (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2)))
786 (\lambda (_: T).(\lambda (t3: T).(or3 (\forall (b: B).(\forall (u0: T).(pr2
787 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T (\lambda (u0: T).(pr0 u1 u0)) (\lambda
788 (u0: T).(pr2 (CHead c0 (Bind Abbr) u0) t1 t3))) (ex3_2 T T (\lambda (y0:
789 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
790 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
791 c0 (Bind Abbr) u1) z t3)))))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead
792 c0 (Bind b) u0) t1 (lift (S O) O t)))) (ex3_2_intro T T (\lambda (u2:
793 T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
794 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3
795 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T
796 (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0)
797 t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind
798 Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_:
799 T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3))))))) x3 x4 H13
800 (pr2_delta c0 d u i H1 u1 x0 H8 x3 H14) (or3_intro2 (\forall (b: B).(\forall
801 (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 x4))) (ex2 T (\lambda (u0: T).(pr0 u1
802 u0)) (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0) t1 x4))) (ex3_2 T T
803 (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0)))
804 (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z:
805 T).(pr2 (CHead c0 (Bind Abbr) u1) z x4)))) (ex3_2_intro T T (\lambda (y0:
806 T).(\lambda (_: T).(pr2 (CHead c0 (Bind Abbr) u1) t1 y0))) (\lambda (y0:
807 T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_: T).(\lambda (z: T).(pr2 (CHead
808 c0 (Bind Abbr) u1) z x4))) x5 x1 (pr2_delta (CHead c0 (Bind Abbr) u1) c0 u1 O
809 (getl_refl Abbr c0 u1) t1 x2 H9 x5 H16) H17 (pr2_delta (CHead c0 (Bind Abbr)
810 u1) d u (S i) (getl_head (Bind Abbr) i c0 (CHead d (Bind Abbr) u) H1 u1) x1
811 x1 (pr0_refl x1) x4 H15)))))))) (pr0_subst0_back x0 x2 x1 O H10 u1 H8)))))))
812 H12)) (subst0_gen_head (Bind Abbr) u x0 x1 t i H11)))))) H_x0)) H_x))))))
813 H6)) (\lambda (H6: (pr0 t1 (lift (S O) O t2))).(or_intror (ex3_2 T T (\lambda
814 (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Abbr) u2 t3)))) (\lambda (u2:
815 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(or3
816 (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3))) (ex2 T
817 (\lambda (u0: T).(pr0 u1 u0)) (\lambda (u0: T).(pr2 (CHead c0 (Bind Abbr) u0)
818 t1 t3))) (ex3_2 T T (\lambda (y0: T).(\lambda (_: T).(pr2 (CHead c0 (Bind
819 Abbr) u1) t1 y0))) (\lambda (y0: T).(\lambda (z: T).(pr0 y0 z))) (\lambda (_:
820 T).(\lambda (z: T).(pr2 (CHead c0 (Bind Abbr) u1) z t3)))))))) (\forall (b:
821 B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))))
822 (\lambda (b: B).(\lambda (u0: T).(pr2_delta (CHead c0 (Bind b) u0) d u (S i)
823 (getl_head (Bind b) i c0 (CHead d (Bind Abbr) u) H1 u0) t1 (lift (S O) O t2)
824 H6 (lift (S O) O t) (subst0_lift_ge_S t2 t u i H3 O (le_O_n i)))))))
825 (pr0_gen_abbr u1 t1 t2 H5)))))))))))))) c y x H0))) H))))).
828 \forall (c: C).(\forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr2 c
829 (THead (Bind Void) u1 t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda
830 (t2: T).(eq T x (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_:
831 T).(pr2 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall
832 (u: T).(pr2 (CHead c (Bind b) u) t1 t2)))))) (\forall (b: B).(\forall (u:
833 T).(pr2 (CHead c (Bind b) u) t1 (lift (S O) O x)))))))))
835 \lambda (c: C).(\lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda
836 (H: (pr2 c (THead (Bind Void) u1 t1) x)).(insert_eq T (THead (Bind Void) u1
837 t1) (\lambda (t: T).(pr2 c t x)) (\lambda (_: T).(or (ex3_2 T T (\lambda (u2:
838 T).(\lambda (t2: T).(eq T x (THead (Bind Void) u2 t2)))) (\lambda (u2:
839 T).(\lambda (_: T).(pr2 c u1 u2))) (\lambda (_: T).(\lambda (t2: T).(\forall
840 (b: B).(\forall (u: T).(pr2 (CHead c (Bind b) u) t1 t2)))))) (\forall (b:
841 B).(\forall (u: T).(pr2 (CHead c (Bind b) u) t1 (lift (S O) O x))))))
842 (\lambda (y: T).(\lambda (H0: (pr2 c y x)).(pr2_ind (\lambda (c0: C).(\lambda
843 (t: T).(\lambda (t0: T).((eq T t (THead (Bind Void) u1 t1)) \to (or (ex3_2 T
844 T (\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Bind Void) u2 t2))))
845 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
846 (t2: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1
847 t2)))))) (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1 (lift
848 (S O) O t0))))))))) (\lambda (c0: C).(\lambda (t0: T).(\lambda (t2:
849 T).(\lambda (H1: (pr0 t0 t2)).(\lambda (H2: (eq T t0 (THead (Bind Void) u1
850 t1))).(let H3 \def (eq_ind T t0 (\lambda (t: T).(pr0 t t2)) H1 (THead (Bind
851 Void) u1 t1) H2) in (or_ind (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq
852 T t2 (THead (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1
853 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O
854 t2)) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind
855 Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda
856 (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind
857 b) u) t1 t3)))))) (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u)
858 t1 (lift (S O) O t2))))) (\lambda (H4: (ex3_2 T T (\lambda (u2: T).(\lambda
859 (t3: T).(eq T t2 (THead (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_:
860 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3))))).(ex3_2_ind
861 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2 t3))))
862 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
863 T).(pr0 t1 t3))) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2
864 (THead (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1
865 u2))) (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2
866 (CHead c0 (Bind b) u) t1 t3)))))) (\forall (b: B).(\forall (u: T).(pr2 (CHead
867 c0 (Bind b) u) t1 (lift (S O) O t2))))) (\lambda (x0: T).(\lambda (x1:
868 T).(\lambda (H5: (eq T t2 (THead (Bind Void) x0 x1))).(\lambda (H6: (pr0 u1
869 x0)).(\lambda (H7: (pr0 t1 x1)).(eq_ind_r T (THead (Bind Void) x0 x1)
870 (\lambda (t: T).(or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t
871 (THead (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1
872 u2))) (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2
873 (CHead c0 (Bind b) u) t1 t3)))))) (\forall (b: B).(\forall (u: T).(pr2 (CHead
874 c0 (Bind b) u) t1 (lift (S O) O t)))))) (or_introl (ex3_2 T T (\lambda (u2:
875 T).(\lambda (t3: T).(eq T (THead (Bind Void) x0 x1) (THead (Bind Void) u2
876 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_:
877 T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b)
878 u) t1 t3)))))) (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1
879 (lift (S O) O (THead (Bind Void) x0 x1))))) (ex3_2_intro T T (\lambda (u2:
880 T).(\lambda (t3: T).(eq T (THead (Bind Void) x0 x1) (THead (Bind Void) u2
881 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_:
882 T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b)
883 u) t1 t3))))) x0 x1 (refl_equal T (THead (Bind Void) x0 x1)) (pr2_free c0 u1
884 x0 H6) (\lambda (b: B).(\lambda (u: T).(pr2_free (CHead c0 (Bind b) u) t1 x1
885 H7))))) t2 H5)))))) H4)) (\lambda (H4: (pr0 t1 (lift (S O) O t2))).(or_intror
886 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2
887 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_:
888 T).(\lambda (t3: T).(\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b)
889 u) t1 t3)))))) (\forall (b: B).(\forall (u: T).(pr2 (CHead c0 (Bind b) u) t1
890 (lift (S O) O t2)))) (\lambda (b: B).(\lambda (u: T).(pr2_free (CHead c0
891 (Bind b) u) t1 (lift (S O) O t2) H4))))) (pr0_gen_void u1 t1 t2 H3))))))))
892 (\lambda (c0: C).(\lambda (d: C).(\lambda (u: T).(\lambda (i: nat).(\lambda
893 (H1: (getl i c0 (CHead d (Bind Abbr) u))).(\lambda (t0: T).(\lambda (t2:
894 T).(\lambda (H2: (pr0 t0 t2)).(\lambda (t: T).(\lambda (H3: (subst0 i u t2
895 t)).(\lambda (H4: (eq T t0 (THead (Bind Void) u1 t1))).(let H5 \def (eq_ind T
896 t0 (\lambda (t3: T).(pr0 t3 t2)) H2 (THead (Bind Void) u1 t1) H4) in (or_ind
897 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2
898 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_:
899 T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O t2)) (or (ex3_2 T T
900 (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Void) u2 t3))))
901 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
902 (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
903 t3)))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
904 (lift (S O) O t))))) (\lambda (H6: (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
905 T).(eq T t2 (THead (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_:
906 T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3))))).(ex3_2_ind
907 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2 t3))))
908 (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3:
909 T).(pr0 t1 t3))) (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t
910 (THead (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1
911 u2))) (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr2
912 (CHead c0 (Bind b) u0) t1 t3)))))) (\forall (b: B).(\forall (u0: T).(pr2
913 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))))) (\lambda (x0: T).(\lambda (x1:
914 T).(\lambda (H7: (eq T t2 (THead (Bind Void) x0 x1))).(\lambda (H8: (pr0 u1
915 x0)).(\lambda (H9: (pr0 t1 x1)).(let H10 \def (eq_ind T t2 (\lambda (t3:
916 T).(subst0 i u t3 t)) H3 (THead (Bind Void) x0 x1) H7) in (or3_ind (ex2 T
917 (\lambda (u2: T).(eq T t (THead (Bind Void) u2 x1))) (\lambda (u2: T).(subst0
918 i u x0 u2))) (ex2 T (\lambda (t3: T).(eq T t (THead (Bind Void) x0 t3)))
919 (\lambda (t3: T).(subst0 (s (Bind Void) i) u x1 t3))) (ex3_2 T T (\lambda
920 (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Void) u2 t3)))) (\lambda (u2:
921 T).(\lambda (_: T).(subst0 i u x0 u2))) (\lambda (_: T).(\lambda (t3:
922 T).(subst0 (s (Bind Void) i) u x1 t3)))) (or (ex3_2 T T (\lambda (u2:
923 T).(\lambda (t3: T).(eq T t (THead (Bind Void) u2 t3)))) (\lambda (u2:
924 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(\forall
925 (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3)))))) (\forall (b:
926 B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t)))))
927 (\lambda (H11: (ex2 T (\lambda (u2: T).(eq T t (THead (Bind Void) u2 x1)))
928 (\lambda (u2: T).(subst0 i u x0 u2)))).(ex2_ind T (\lambda (u2: T).(eq T t
929 (THead (Bind Void) u2 x1))) (\lambda (u2: T).(subst0 i u x0 u2)) (or (ex3_2 T
930 T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Void) u2 t3))))
931 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
932 (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
933 t3)))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
934 (lift (S O) O t))))) (\lambda (x2: T).(\lambda (H12: (eq T t (THead (Bind
935 Void) x2 x1))).(\lambda (H13: (subst0 i u x0 x2)).(or_introl (ex3_2 T T
936 (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Void) u2 t3))))
937 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
938 (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
939 t3)))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
940 (lift (S O) O t)))) (ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T
941 t (THead (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1
942 u2))) (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr2
943 (CHead c0 (Bind b) u0) t1 t3))))) x2 x1 H12 (pr2_delta c0 d u i H1 u1 x0 H8
944 x2 H13) (\lambda (b: B).(\lambda (u0: T).(pr2_free (CHead c0 (Bind b) u0) t1
945 x1 H9)))))))) H11)) (\lambda (H11: (ex2 T (\lambda (t3: T).(eq T t (THead
946 (Bind Void) x0 t3))) (\lambda (t3: T).(subst0 (s (Bind Void) i) u x1
947 t3)))).(ex2_ind T (\lambda (t3: T).(eq T t (THead (Bind Void) x0 t3)))
948 (\lambda (t3: T).(subst0 (s (Bind Void) i) u x1 t3)) (or (ex3_2 T T (\lambda
949 (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Void) u2 t3)))) (\lambda (u2:
950 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(\forall
951 (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3)))))) (\forall (b:
952 B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t)))))
953 (\lambda (x2: T).(\lambda (H12: (eq T t (THead (Bind Void) x0 x2))).(\lambda
954 (H13: (subst0 (s (Bind Void) i) u x1 x2)).(or_introl (ex3_2 T T (\lambda (u2:
955 T).(\lambda (t3: T).(eq T t (THead (Bind Void) u2 t3)))) (\lambda (u2:
956 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(\forall
957 (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3)))))) (\forall (b:
958 B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))))
959 (ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Void)
960 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_:
961 T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b)
962 u0) t1 t3))))) x0 x2 H12 (pr2_free c0 u1 x0 H8) (\lambda (b: B).(\lambda (u0:
963 T).(pr2_delta (CHead c0 (Bind b) u0) d u (S i) (getl_head (Bind b) i c0
964 (CHead d (Bind Abbr) u) H1 u0) t1 x1 H9 x2 H13)))))))) H11)) (\lambda (H11:
965 (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Void) u2
966 t3)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i u x0 u2))) (\lambda (_:
967 T).(\lambda (t3: T).(subst0 (s (Bind Void) i) u x1 t3))))).(ex3_2_ind T T
968 (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Void) u2 t3))))
969 (\lambda (u2: T).(\lambda (_: T).(subst0 i u x0 u2))) (\lambda (_:
970 T).(\lambda (t3: T).(subst0 (s (Bind Void) i) u x1 t3))) (or (ex3_2 T T
971 (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Void) u2 t3))))
972 (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda
973 (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
974 t3)))))) (\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1
975 (lift (S O) O t))))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H12: (eq T t
976 (THead (Bind Void) x2 x3))).(\lambda (H13: (subst0 i u x0 x2)).(\lambda (H14:
977 (subst0 (s (Bind Void) i) u x1 x3)).(or_introl (ex3_2 T T (\lambda (u2:
978 T).(\lambda (t3: T).(eq T t (THead (Bind Void) u2 t3)))) (\lambda (u2:
979 T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(\forall
980 (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 t3)))))) (\forall (b:
981 B).(\forall (u0: T).(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t))))
982 (ex3_2_intro T T (\lambda (u2: T).(\lambda (t3: T).(eq T t (THead (Bind Void)
983 u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2 c0 u1 u2))) (\lambda (_:
984 T).(\lambda (t3: T).(\forall (b: B).(\forall (u0: T).(pr2 (CHead c0 (Bind b)
985 u0) t1 t3))))) x2 x3 H12 (pr2_delta c0 d u i H1 u1 x0 H8 x2 H13) (\lambda (b:
986 B).(\lambda (u0: T).(pr2_delta (CHead c0 (Bind b) u0) d u (S i) (getl_head
987 (Bind b) i c0 (CHead d (Bind Abbr) u) H1 u0) t1 x1 H9 x3 H14)))))))))) H11))
988 (subst0_gen_head (Bind Void) u x0 x1 t i H10)))))))) H6)) (\lambda (H6: (pr0
989 t1 (lift (S O) O t2))).(or_intror (ex3_2 T T (\lambda (u2: T).(\lambda (t3:
990 T).(eq T t (THead (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr2
991 c0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(\forall (b: B).(\forall (u0:
992 T).(pr2 (CHead c0 (Bind b) u0) t1 t3)))))) (\forall (b: B).(\forall (u0:
993 T).(pr2 (CHead c0 (Bind b) u0) t1 (lift (S O) O t)))) (\lambda (b:
994 B).(\lambda (u0: T).(pr2_delta (CHead c0 (Bind b) u0) d u (S i) (getl_head
995 (Bind b) i c0 (CHead d (Bind Abbr) u) H1 u0) t1 (lift (S O) O t2) H6 (lift (S
996 O) O t) (subst0_lift_ge_S t2 t u i H3 O (le_O_n i))))))) (pr0_gen_void u1 t1
997 t2 H5)))))))))))))) c y x H0))) H))))).
projects / helm.git / blob