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