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