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