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