(* This file was automatically generated: do not edit *********************)
+include "LambdaDelta-1/pr0/defs.ma".
-
-include "pr0/defs.ma".
-
-include "subst0/subst0.ma".
+include "LambdaDelta-1/subst0/subst0.ma".
theorem pr0_lift:
\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (h: nat).(\forall
(lift h d t0)))))) (\lambda (t: T).(\lambda (h: nat).(\lambda (d:
nat).(pr0_refl (lift h d t))))) (\lambda (u1: T).(\lambda (u2: T).(\lambda
(_: (pr0 u1 u2)).(\lambda (H1: ((\forall (h: nat).(\forall (d: nat).(pr0
-(lift h d u1) (lift h d u2)))))).(\lambda (t0: T).(\lambda (t3: T).(\lambda
-(_: (pr0 t0 t3)).(\lambda (H3: ((\forall (h: nat).(\forall (d: nat).(pr0
-(lift h d t0) (lift h d t3)))))).(\lambda (k: K).(\lambda (h: nat).(\lambda
-(d: nat).(eq_ind_r T (THead k (lift h d u1) (lift h (s k d) t0)) (\lambda (t:
-T).(pr0 t (lift h d (THead k u2 t3)))) (eq_ind_r T (THead k (lift h d u2)
-(lift h (s k d) t3)) (\lambda (t: T).(pr0 (THead k (lift h d u1) (lift h (s k
-d) t0)) t)) (pr0_comp (lift h d u1) (lift h d u2) (H1 h d) (lift h (s k d)
-t0) (lift h (s k d) t3) (H3 h (s k d)) k) (lift h d (THead k u2 t3))
-(lift_head k u2 t3 h d)) (lift h d (THead k u1 t0)) (lift_head k u1 t0 h
+(lift h d u1) (lift h d u2)))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda
+(_: (pr0 t3 t4)).(\lambda (H3: ((\forall (h: nat).(\forall (d: nat).(pr0
+(lift h d t3) (lift h d t4)))))).(\lambda (k: K).(\lambda (h: nat).(\lambda
+(d: nat).(eq_ind_r T (THead k (lift h d u1) (lift h (s k d) t3)) (\lambda (t:
+T).(pr0 t (lift h d (THead k u2 t4)))) (eq_ind_r T (THead k (lift h d u2)
+(lift h (s k d) t4)) (\lambda (t: T).(pr0 (THead k (lift h d u1) (lift h (s k
+d) t3)) t)) (pr0_comp (lift h d u1) (lift h d u2) (H1 h d) (lift h (s k d)
+t3) (lift h (s k d) t4) (H3 h (s k d)) k) (lift h d (THead k u2 t4))
+(lift_head k u2 t4 h d)) (lift h d (THead k u1 t3)) (lift_head k u1 t3 h
d))))))))))))) (\lambda (u: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_:
(pr0 v1 v2)).(\lambda (H1: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h
-d v1) (lift h d v2)))))).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (pr0
-t0 t3)).(\lambda (H3: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t0)
-(lift h d t3)))))).(\lambda (h: nat).(\lambda (d: nat).(eq_ind_r T (THead
+d v1) (lift h d v2)))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0
+t3 t4)).(\lambda (H3: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t3)
+(lift h d t4)))))).(\lambda (h: nat).(\lambda (d: nat).(eq_ind_r T (THead
(Flat Appl) (lift h d v1) (lift h (s (Flat Appl) d) (THead (Bind Abst) u
-t0))) (\lambda (t: T).(pr0 t (lift h d (THead (Bind Abbr) v2 t3)))) (eq_ind_r
+t3))) (\lambda (t: T).(pr0 t (lift h d (THead (Bind Abbr) v2 t4)))) (eq_ind_r
T (THead (Bind Abst) (lift h (s (Flat Appl) d) u) (lift h (s (Bind Abst) (s
-(Flat Appl) d)) t0)) (\lambda (t: T).(pr0 (THead (Flat Appl) (lift h d v1) t)
-(lift h d (THead (Bind Abbr) v2 t3)))) (eq_ind_r T (THead (Bind Abbr) (lift h
-d v2) (lift h (s (Bind Abbr) d) t3)) (\lambda (t: T).(pr0 (THead (Flat Appl)
+(Flat Appl) d)) t3)) (\lambda (t: T).(pr0 (THead (Flat Appl) (lift h d v1) t)
+(lift h d (THead (Bind Abbr) v2 t4)))) (eq_ind_r T (THead (Bind Abbr) (lift h
+d v2) (lift h (s (Bind Abbr) d) t4)) (\lambda (t: T).(pr0 (THead (Flat Appl)
(lift h d v1) (THead (Bind Abst) (lift h (s (Flat Appl) d) u) (lift h (s
-(Bind Abst) (s (Flat Appl) d)) t0))) t)) (pr0_beta (lift h (s (Flat Appl) d)
+(Bind Abst) (s (Flat Appl) d)) t3))) t)) (pr0_beta (lift h (s (Flat Appl) d)
u) (lift h d v1) (lift h d v2) (H1 h d) (lift h (s (Bind Abst) (s (Flat Appl)
-d)) t0) (lift h (s (Bind Abbr) d) t3) (H3 h (s (Bind Abbr) d))) (lift h d
-(THead (Bind Abbr) v2 t3)) (lift_head (Bind Abbr) v2 t3 h d)) (lift h (s
-(Flat Appl) d) (THead (Bind Abst) u t0)) (lift_head (Bind Abst) u t0 h (s
-(Flat Appl) d))) (lift h d (THead (Flat Appl) v1 (THead (Bind Abst) u t0)))
-(lift_head (Flat Appl) v1 (THead (Bind Abst) u t0) h d))))))))))))) (\lambda
+d)) t3) (lift h (s (Bind Abbr) d) t4) (H3 h (s (Bind Abbr) d))) (lift h d
+(THead (Bind Abbr) v2 t4)) (lift_head (Bind Abbr) v2 t4 h d)) (lift h (s
+(Flat Appl) d) (THead (Bind Abst) u t3)) (lift_head (Bind Abst) u t3 h (s
+(Flat Appl) d))) (lift h d (THead (Flat Appl) v1 (THead (Bind Abst) u t3)))
+(lift_head (Flat Appl) v1 (THead (Bind Abst) u t3) h d))))))))))))) (\lambda
(b: B).(\lambda (H0: (not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2:
T).(\lambda (_: (pr0 v1 v2)).(\lambda (H2: ((\forall (h: nat).(\forall (d:
nat).(pr0 (lift h d v1) (lift h d v2)))))).(\lambda (u1: T).(\lambda (u2:
T).(\lambda (_: (pr0 u1 u2)).(\lambda (H4: ((\forall (h: nat).(\forall (d:
-nat).(pr0 (lift h d u1) (lift h d u2)))))).(\lambda (t0: T).(\lambda (t3:
-T).(\lambda (_: (pr0 t0 t3)).(\lambda (H6: ((\forall (h: nat).(\forall (d:
-nat).(pr0 (lift h d t0) (lift h d t3)))))).(\lambda (h: nat).(\lambda (d:
+nat).(pr0 (lift h d u1) (lift h d u2)))))).(\lambda (t3: T).(\lambda (t4:
+T).(\lambda (_: (pr0 t3 t4)).(\lambda (H6: ((\forall (h: nat).(\forall (d:
+nat).(pr0 (lift h d t3) (lift h d t4)))))).(\lambda (h: nat).(\lambda (d:
nat).(eq_ind_r T (THead (Flat Appl) (lift h d v1) (lift h (s (Flat Appl) d)
-(THead (Bind b) u1 t0))) (\lambda (t: T).(pr0 t (lift h d (THead (Bind b) u2
-(THead (Flat Appl) (lift (S O) O v2) t3))))) (eq_ind_r T (THead (Bind b)
-(lift h (s (Flat Appl) d) u1) (lift h (s (Bind b) (s (Flat Appl) d)) t0))
+(THead (Bind b) u1 t3))) (\lambda (t: T).(pr0 t (lift h d (THead (Bind b) u2
+(THead (Flat Appl) (lift (S O) O v2) t4))))) (eq_ind_r T (THead (Bind b)
+(lift h (s (Flat Appl) d) u1) (lift h (s (Bind b) (s (Flat Appl) d)) t3))
(\lambda (t: T).(pr0 (THead (Flat Appl) (lift h d v1) t) (lift h d (THead
-(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t3))))) (eq_ind_r T (THead
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))))) (eq_ind_r T (THead
(Bind b) (lift h d u2) (lift h (s (Bind b) d) (THead (Flat Appl) (lift (S O)
-O v2) t3))) (\lambda (t: T).(pr0 (THead (Flat Appl) (lift h d v1) (THead
+O v2) t4))) (\lambda (t: T).(pr0 (THead (Flat Appl) (lift h d v1) (THead
(Bind b) (lift h (s (Flat Appl) d) u1) (lift h (s (Bind b) (s (Flat Appl) d))
-t0))) t)) (eq_ind_r T (THead (Flat Appl) (lift h (s (Bind b) d) (lift (S O) O
-v2)) (lift h (s (Flat Appl) (s (Bind b) d)) t3)) (\lambda (t: T).(pr0 (THead
+t3))) t)) (eq_ind_r T (THead (Flat Appl) (lift h (s (Bind b) d) (lift (S O) O
+v2)) (lift h (s (Flat Appl) (s (Bind b) d)) t4)) (\lambda (t: T).(pr0 (THead
(Flat Appl) (lift h d v1) (THead (Bind b) (lift h (s (Flat Appl) d) u1) (lift
-h (s (Bind b) (s (Flat Appl) d)) t0))) (THead (Bind b) (lift h d u2) t)))
+h (s (Bind b) (s (Flat Appl) d)) t3))) (THead (Bind b) (lift h d u2) t)))
(eq_ind nat (plus (S O) d) (\lambda (n: nat).(pr0 (THead (Flat Appl) (lift h
-d v1) (THead (Bind b) (lift h d u1) (lift h n t0))) (THead (Bind b) (lift h d
-u2) (THead (Flat Appl) (lift h n (lift (S O) O v2)) (lift h n t3)))))
+d v1) (THead (Bind b) (lift h d u1) (lift h n t3))) (THead (Bind b) (lift h d
+u2) (THead (Flat Appl) (lift h n (lift (S O) O v2)) (lift h n t4)))))
(eq_ind_r T (lift (S O) O (lift h d v2)) (\lambda (t: T).(pr0 (THead (Flat
Appl) (lift h d v1) (THead (Bind b) (lift h d u1) (lift h (plus (S O) d)
-t0))) (THead (Bind b) (lift h d u2) (THead (Flat Appl) t (lift h (plus (S O)
-d) t3))))) (pr0_upsilon b H0 (lift h d v1) (lift h d v2) (H2 h d) (lift h d
-u1) (lift h d u2) (H4 h d) (lift h (plus (S O) d) t0) (lift h (plus (S O) d)
-t3) (H6 h (plus (S O) d))) (lift h (plus (S O) d) (lift (S O) O v2)) (lift_d
+t3))) (THead (Bind b) (lift h d u2) (THead (Flat Appl) t (lift h (plus (S O)
+d) t4))))) (pr0_upsilon b H0 (lift h d v1) (lift h d v2) (H2 h d) (lift h d
+u1) (lift h d u2) (H4 h d) (lift h (plus (S O) d) t3) (lift h (plus (S O) d)
+t4) (H6 h (plus (S O) d))) (lift h (plus (S O) d) (lift (S O) O v2)) (lift_d
v2 h (S O) d O (le_O_n d))) (S d) (refl_equal nat (S d))) (lift h (s (Bind b)
-d) (THead (Flat Appl) (lift (S O) O v2) t3)) (lift_head (Flat Appl) (lift (S
-O) O v2) t3 h (s (Bind b) d))) (lift h d (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t3))) (lift_head (Bind b) u2 (THead (Flat Appl) (lift
-(S O) O v2) t3) h d)) (lift h (s (Flat Appl) d) (THead (Bind b) u1 t0))
-(lift_head (Bind b) u1 t0 h (s (Flat Appl) d))) (lift h d (THead (Flat Appl)
-v1 (THead (Bind b) u1 t0))) (lift_head (Flat Appl) v1 (THead (Bind b) u1 t0)
+d) (THead (Flat Appl) (lift (S O) O v2) t4)) (lift_head (Flat Appl) (lift (S
+O) O v2) t4 h (s (Bind b) d))) (lift h d (THead (Bind b) u2 (THead (Flat
+Appl) (lift (S O) O v2) t4))) (lift_head (Bind b) u2 (THead (Flat Appl) (lift
+(S O) O v2) t4) h d)) (lift h (s (Flat Appl) d) (THead (Bind b) u1 t3))
+(lift_head (Bind b) u1 t3 h (s (Flat Appl) d))) (lift h d (THead (Flat Appl)
+v1 (THead (Bind b) u1 t3))) (lift_head (Flat Appl) v1 (THead (Bind b) u1 t3)
h d)))))))))))))))))) (\lambda (u1: T).(\lambda (u2: T).(\lambda (_: (pr0 u1
u2)).(\lambda (H1: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d u1)
-(lift h d u2)))))).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (pr0 t0
-t3)).(\lambda (H3: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t0)
-(lift h d t3)))))).(\lambda (w: T).(\lambda (H4: (subst0 O u2 t3 w)).(\lambda
+(lift h d u2)))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3
+t4)).(\lambda (H3: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t3)
+(lift h d t4)))))).(\lambda (w: T).(\lambda (H4: (subst0 O u2 t4 w)).(\lambda
(h: nat).(\lambda (d: nat).(eq_ind_r T (THead (Bind Abbr) (lift h d u1) (lift
-h (s (Bind Abbr) d) t0)) (\lambda (t: T).(pr0 t (lift h d (THead (Bind Abbr)
+h (s (Bind Abbr) d) t3)) (\lambda (t: T).(pr0 t (lift h d (THead (Bind Abbr)
u2 w)))) (eq_ind_r T (THead (Bind Abbr) (lift h d u2) (lift h (s (Bind Abbr)
d) w)) (\lambda (t: T).(pr0 (THead (Bind Abbr) (lift h d u1) (lift h (s (Bind
-Abbr) d) t0)) t)) (pr0_delta (lift h d u1) (lift h d u2) (H1 h d) (lift h (S
-d) t0) (lift h (S d) t3) (H3 h (S d)) (lift h (S d) w) (let d' \def (S d) in
+Abbr) d) t3)) t)) (pr0_delta (lift h d u1) (lift h d u2) (H1 h d) (lift h (S
+d) t3) (lift h (S d) t4) (H3 h (S d)) (lift h (S d) w) (let d' \def (S d) in
(eq_ind nat (minus (S d) (S O)) (\lambda (n: nat).(subst0 O (lift h n u2)
-(lift h d' t3) (lift h d' w))) (subst0_lift_lt t3 w u2 O H4 (S d) (le_n_S O d
+(lift h d' t4) (lift h d' w))) (subst0_lift_lt t4 w u2 O H4 (S d) (le_n_S O d
(le_O_n d)) h) d (eq_ind nat d (\lambda (n: nat).(eq nat n d)) (refl_equal
nat d) (minus d O) (minus_n_O d))))) (lift h d (THead (Bind Abbr) u2 w))
-(lift_head (Bind Abbr) u2 w h d)) (lift h d (THead (Bind Abbr) u1 t0))
-(lift_head (Bind Abbr) u1 t0 h d)))))))))))))) (\lambda (b: B).(\lambda (H0:
-(not (eq B b Abst))).(\lambda (t0: T).(\lambda (t3: T).(\lambda (_: (pr0 t0
-t3)).(\lambda (H2: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t0)
-(lift h d t3)))))).(\lambda (u: T).(\lambda (h: nat).(\lambda (d:
+(lift_head (Bind Abbr) u2 w h d)) (lift h d (THead (Bind Abbr) u1 t3))
+(lift_head (Bind Abbr) u1 t3 h d)))))))))))))) (\lambda (b: B).(\lambda (H0:
+(not (eq B b Abst))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (_: (pr0 t3
+t4)).(\lambda (H2: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t3)
+(lift h d t4)))))).(\lambda (u: T).(\lambda (h: nat).(\lambda (d:
nat).(eq_ind_r T (THead (Bind b) (lift h d u) (lift h (s (Bind b) d) (lift (S
-O) O t0))) (\lambda (t: T).(pr0 t (lift h d t3))) (eq_ind nat (plus (S O) d)
+O) O t3))) (\lambda (t: T).(pr0 t (lift h d t4))) (eq_ind nat (plus (S O) d)
(\lambda (n: nat).(pr0 (THead (Bind b) (lift h d u) (lift h n (lift (S O) O
-t0))) (lift h d t3))) (eq_ind_r T (lift (S O) O (lift h d t0)) (\lambda (t:
-T).(pr0 (THead (Bind b) (lift h d u) t) (lift h d t3))) (pr0_zeta b H0 (lift
-h d t0) (lift h d t3) (H2 h d) (lift h d u)) (lift h (plus (S O) d) (lift (S
-O) O t0)) (lift_d t0 h (S O) d O (le_O_n d))) (S d) (refl_equal nat (S d)))
-(lift h d (THead (Bind b) u (lift (S O) O t0))) (lift_head (Bind b) u (lift
-(S O) O t0) h d))))))))))) (\lambda (t0: T).(\lambda (t3: T).(\lambda (_:
-(pr0 t0 t3)).(\lambda (H1: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h
-d t0) (lift h d t3)))))).(\lambda (u: T).(\lambda (h: nat).(\lambda (d:
+t3))) (lift h d t4))) (eq_ind_r T (lift (S O) O (lift h d t3)) (\lambda (t:
+T).(pr0 (THead (Bind b) (lift h d u) t) (lift h d t4))) (pr0_zeta b H0 (lift
+h d t3) (lift h d t4) (H2 h d) (lift h d u)) (lift h (plus (S O) d) (lift (S
+O) O t3)) (lift_d t3 h (S O) d O (le_O_n d))) (S d) (refl_equal nat (S d)))
+(lift h d (THead (Bind b) u (lift (S O) O t3))) (lift_head (Bind b) u (lift
+(S O) O t3) h d))))))))))) (\lambda (t3: T).(\lambda (t4: T).(\lambda (_:
+(pr0 t3 t4)).(\lambda (H1: ((\forall (h: nat).(\forall (d: nat).(pr0 (lift h
+d t3) (lift h d t4)))))).(\lambda (u: T).(\lambda (h: nat).(\lambda (d:
nat).(eq_ind_r T (THead (Flat Cast) (lift h d u) (lift h (s (Flat Cast) d)
-t0)) (\lambda (t: T).(pr0 t (lift h d t3))) (pr0_epsilon (lift h (s (Flat
-Cast) d) t0) (lift h d t3) (H1 h d) (lift h d u)) (lift h d (THead (Flat
-Cast) u t0)) (lift_head (Flat Cast) u t0 h d))))))))) t1 t2 H))).
+t3)) (\lambda (t: T).(pr0 t (lift h d t4))) (pr0_tau (lift h (s (Flat Cast)
+d) t3) (lift h d t4) (H1 h d) (lift h d u)) (lift h d (THead (Flat Cast) u
+t3)) (lift_head (Flat Cast) u t3 h d))))))))) t1 t2 H))).
theorem pr0_subst0_back:
\forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst0
(\lambda (v: T).(\lambda (i0: nat).(\lambda (u1: T).(\lambda (H0: (pr0 u1
v)).(ex_intro2 T (\lambda (t: T).(subst0 i0 u1 (TLRef i0) t)) (\lambda (t:
T).(pr0 t (lift (S i0) O v))) (lift (S i0) O u1) (subst0_lref u1 i0)
-(pr0_lift u1 v H0 (S i0) O)))))) (\lambda (v: T).(\lambda (u0: T).(\lambda
-(u1: T).(\lambda (i0: nat).(\lambda (_: (subst0 i0 v u1 u0)).(\lambda (H1:
-((\forall (u3: T).((pr0 u3 v) \to (ex2 T (\lambda (t: T).(subst0 i0 u3 u1 t))
-(\lambda (t: T).(pr0 t u0))))))).(\lambda (t: T).(\lambda (k: K).(\lambda
-(u3: T).(\lambda (H2: (pr0 u3 v)).(ex2_ind T (\lambda (t0: T).(subst0 i0 u3
-u1 t0)) (\lambda (t0: T).(pr0 t0 u0)) (ex2 T (\lambda (t0: T).(subst0 i0 u3
-(THead k u1 t) t0)) (\lambda (t0: T).(pr0 t0 (THead k u0 t)))) (\lambda (x:
-T).(\lambda (H3: (subst0 i0 u3 u1 x)).(\lambda (H4: (pr0 x u0)).(ex_intro2 T
-(\lambda (t0: T).(subst0 i0 u3 (THead k u1 t) t0)) (\lambda (t0: T).(pr0 t0
-(THead k u0 t))) (THead k x t) (subst0_fst u3 x u1 i0 H3 t k) (pr0_comp x u0
-H4 t t (pr0_refl t) k))))) (H1 u3 H2)))))))))))) (\lambda (k: K).(\lambda (v:
-T).(\lambda (t0: T).(\lambda (t3: T).(\lambda (i0: nat).(\lambda (_: (subst0
-(s k i0) v t3 t0)).(\lambda (H1: ((\forall (u1: T).((pr0 u1 v) \to (ex2 T
-(\lambda (t: T).(subst0 (s k i0) u1 t3 t)) (\lambda (t: T).(pr0 t
-t0))))))).(\lambda (u: T).(\lambda (u1: T).(\lambda (H2: (pr0 u1 v)).(ex2_ind
-T (\lambda (t: T).(subst0 (s k i0) u1 t3 t)) (\lambda (t: T).(pr0 t t0)) (ex2
-T (\lambda (t: T).(subst0 i0 u1 (THead k u t3) t)) (\lambda (t: T).(pr0 t
-(THead k u t0)))) (\lambda (x: T).(\lambda (H3: (subst0 (s k i0) u1 t3
-x)).(\lambda (H4: (pr0 x t0)).(ex_intro2 T (\lambda (t: T).(subst0 i0 u1
-(THead k u t3) t)) (\lambda (t: T).(pr0 t (THead k u t0))) (THead k u x)
-(subst0_snd k u1 x t3 i0 H3 u) (pr0_comp u u (pr0_refl u) x t0 H4 k))))) (H1
-u1 H2)))))))))))) (\lambda (v: T).(\lambda (u1: T).(\lambda (u0: T).(\lambda
-(i0: nat).(\lambda (_: (subst0 i0 v u1 u0)).(\lambda (H1: ((\forall (u3:
-T).((pr0 u3 v) \to (ex2 T (\lambda (t: T).(subst0 i0 u3 u1 t)) (\lambda (t:
-T).(pr0 t u0))))))).(\lambda (k: K).(\lambda (t0: T).(\lambda (t3:
-T).(\lambda (_: (subst0 (s k i0) v t0 t3)).(\lambda (H3: ((\forall (u3:
-T).((pr0 u3 v) \to (ex2 T (\lambda (t: T).(subst0 (s k i0) u3 t0 t)) (\lambda
-(t: T).(pr0 t t3))))))).(\lambda (u3: T).(\lambda (H4: (pr0 u3 v)).(ex2_ind T
-(\lambda (t: T).(subst0 (s k i0) u3 t0 t)) (\lambda (t: T).(pr0 t t3)) (ex2 T
-(\lambda (t: T).(subst0 i0 u3 (THead k u1 t0) t)) (\lambda (t: T).(pr0 t
-(THead k u0 t3)))) (\lambda (x: T).(\lambda (H5: (subst0 (s k i0) u3 t0
-x)).(\lambda (H6: (pr0 x t3)).(ex2_ind T (\lambda (t: T).(subst0 i0 u3 u1 t))
-(\lambda (t: T).(pr0 t u0)) (ex2 T (\lambda (t: T).(subst0 i0 u3 (THead k u1
-t0) t)) (\lambda (t: T).(pr0 t (THead k u0 t3)))) (\lambda (x0: T).(\lambda
-(H7: (subst0 i0 u3 u1 x0)).(\lambda (H8: (pr0 x0 u0)).(ex_intro2 T (\lambda
-(t: T).(subst0 i0 u3 (THead k u1 t0) t)) (\lambda (t: T).(pr0 t (THead k u0
-t3))) (THead k x0 x) (subst0_both u3 u1 x0 i0 H7 k t0 x H5) (pr0_comp x0 u0
-H8 x t3 H6 k))))) (H1 u3 H4))))) (H3 u3 H4))))))))))))))) i u2 t1 t2 H))))).
+(pr0_lift u1 v H0 (S i0) O)))))) (\lambda (v: T).(\lambda (u3: T).(\lambda
+(u1: T).(\lambda (i0: nat).(\lambda (_: (subst0 i0 v u1 u3)).(\lambda (H1:
+((\forall (u4: T).((pr0 u4 v) \to (ex2 T (\lambda (t: T).(subst0 i0 u4 u1 t))
+(\lambda (t: T).(pr0 t u3))))))).(\lambda (t: T).(\lambda (k: K).(\lambda
+(u0: T).(\lambda (H2: (pr0 u0 v)).(ex2_ind T (\lambda (t0: T).(subst0 i0 u0
+u1 t0)) (\lambda (t0: T).(pr0 t0 u3)) (ex2 T (\lambda (t0: T).(subst0 i0 u0
+(THead k u1 t) t0)) (\lambda (t0: T).(pr0 t0 (THead k u3 t)))) (\lambda (x:
+T).(\lambda (H3: (subst0 i0 u0 u1 x)).(\lambda (H4: (pr0 x u3)).(ex_intro2 T
+(\lambda (t0: T).(subst0 i0 u0 (THead k u1 t) t0)) (\lambda (t0: T).(pr0 t0
+(THead k u3 t))) (THead k x t) (subst0_fst u0 x u1 i0 H3 t k) (pr0_comp x u3
+H4 t t (pr0_refl t) k))))) (H1 u0 H2)))))))))))) (\lambda (k: K).(\lambda (v:
+T).(\lambda (t3: T).(\lambda (t4: T).(\lambda (i0: nat).(\lambda (_: (subst0
+(s k i0) v t4 t3)).(\lambda (H1: ((\forall (u1: T).((pr0 u1 v) \to (ex2 T
+(\lambda (t: T).(subst0 (s k i0) u1 t4 t)) (\lambda (t: T).(pr0 t
+t3))))))).(\lambda (u: T).(\lambda (u1: T).(\lambda (H2: (pr0 u1 v)).(ex2_ind
+T (\lambda (t: T).(subst0 (s k i0) u1 t4 t)) (\lambda (t: T).(pr0 t t3)) (ex2
+T (\lambda (t: T).(subst0 i0 u1 (THead k u t4) t)) (\lambda (t: T).(pr0 t
+(THead k u t3)))) (\lambda (x: T).(\lambda (H3: (subst0 (s k i0) u1 t4
+x)).(\lambda (H4: (pr0 x t3)).(ex_intro2 T (\lambda (t: T).(subst0 i0 u1
+(THead k u t4) t)) (\lambda (t: T).(pr0 t (THead k u t3))) (THead k u x)
+(subst0_snd k u1 x t4 i0 H3 u) (pr0_comp u u (pr0_refl u) x t3 H4 k))))) (H1
+u1 H2)))))))))))) (\lambda (v: T).(\lambda (u1: T).(\lambda (u3: T).(\lambda
+(i0: nat).(\lambda (_: (subst0 i0 v u1 u3)).(\lambda (H1: ((\forall (u4:
+T).((pr0 u4 v) \to (ex2 T (\lambda (t: T).(subst0 i0 u4 u1 t)) (\lambda (t:
+T).(pr0 t u3))))))).(\lambda (k: K).(\lambda (t3: T).(\lambda (t4:
+T).(\lambda (_: (subst0 (s k i0) v t3 t4)).(\lambda (H3: ((\forall (u4:
+T).((pr0 u4 v) \to (ex2 T (\lambda (t: T).(subst0 (s k i0) u4 t3 t)) (\lambda
+(t: T).(pr0 t t4))))))).(\lambda (u0: T).(\lambda (H4: (pr0 u0 v)).(ex2_ind T
+(\lambda (t: T).(subst0 (s k i0) u0 t3 t)) (\lambda (t: T).(pr0 t t4)) (ex2 T
+(\lambda (t: T).(subst0 i0 u0 (THead k u1 t3) t)) (\lambda (t: T).(pr0 t
+(THead k u3 t4)))) (\lambda (x: T).(\lambda (H5: (subst0 (s k i0) u0 t3
+x)).(\lambda (H6: (pr0 x t4)).(ex2_ind T (\lambda (t: T).(subst0 i0 u0 u1 t))
+(\lambda (t: T).(pr0 t u3)) (ex2 T (\lambda (t: T).(subst0 i0 u0 (THead k u1
+t3) t)) (\lambda (t: T).(pr0 t (THead k u3 t4)))) (\lambda (x0: T).(\lambda
+(H7: (subst0 i0 u0 u1 x0)).(\lambda (H8: (pr0 x0 u3)).(ex_intro2 T (\lambda
+(t: T).(subst0 i0 u0 (THead k u1 t3) t)) (\lambda (t: T).(pr0 t (THead k u3
+t4))) (THead k x0 x) (subst0_both u0 u1 x0 i0 H7 k t3 x H5) (pr0_comp x0 u3
+H8 x t4 H6 k))))) (H1 u0 H4))))) (H3 u0 H4))))))))))))))) i u2 t1 t2 H))))).
theorem pr0_subst0_fwd:
\forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst0
(\lambda (v: T).(\lambda (i0: nat).(\lambda (u1: T).(\lambda (H0: (pr0 v
u1)).(ex_intro2 T (\lambda (t: T).(subst0 i0 u1 (TLRef i0) t)) (\lambda (t:
T).(pr0 (lift (S i0) O v) t)) (lift (S i0) O u1) (subst0_lref u1 i0)
-(pr0_lift v u1 H0 (S i0) O)))))) (\lambda (v: T).(\lambda (u0: T).(\lambda
-(u1: T).(\lambda (i0: nat).(\lambda (_: (subst0 i0 v u1 u0)).(\lambda (H1:
-((\forall (u3: T).((pr0 v u3) \to (ex2 T (\lambda (t: T).(subst0 i0 u3 u1 t))
-(\lambda (t: T).(pr0 u0 t))))))).(\lambda (t: T).(\lambda (k: K).(\lambda
-(u3: T).(\lambda (H2: (pr0 v u3)).(ex2_ind T (\lambda (t0: T).(subst0 i0 u3
-u1 t0)) (\lambda (t0: T).(pr0 u0 t0)) (ex2 T (\lambda (t0: T).(subst0 i0 u3
-(THead k u1 t) t0)) (\lambda (t0: T).(pr0 (THead k u0 t) t0))) (\lambda (x:
-T).(\lambda (H3: (subst0 i0 u3 u1 x)).(\lambda (H4: (pr0 u0 x)).(ex_intro2 T
-(\lambda (t0: T).(subst0 i0 u3 (THead k u1 t) t0)) (\lambda (t0: T).(pr0
-(THead k u0 t) t0)) (THead k x t) (subst0_fst u3 x u1 i0 H3 t k) (pr0_comp u0
-x H4 t t (pr0_refl t) k))))) (H1 u3 H2)))))))))))) (\lambda (k: K).(\lambda
-(v: T).(\lambda (t0: T).(\lambda (t3: T).(\lambda (i0: nat).(\lambda (_:
-(subst0 (s k i0) v t3 t0)).(\lambda (H1: ((\forall (u1: T).((pr0 v u1) \to
-(ex2 T (\lambda (t: T).(subst0 (s k i0) u1 t3 t)) (\lambda (t: T).(pr0 t0
+(pr0_lift v u1 H0 (S i0) O)))))) (\lambda (v: T).(\lambda (u3: T).(\lambda
+(u1: T).(\lambda (i0: nat).(\lambda (_: (subst0 i0 v u1 u3)).(\lambda (H1:
+((\forall (u4: T).((pr0 v u4) \to (ex2 T (\lambda (t: T).(subst0 i0 u4 u1 t))
+(\lambda (t: T).(pr0 u3 t))))))).(\lambda (t: T).(\lambda (k: K).(\lambda
+(u0: T).(\lambda (H2: (pr0 v u0)).(ex2_ind T (\lambda (t0: T).(subst0 i0 u0
+u1 t0)) (\lambda (t0: T).(pr0 u3 t0)) (ex2 T (\lambda (t0: T).(subst0 i0 u0
+(THead k u1 t) t0)) (\lambda (t0: T).(pr0 (THead k u3 t) t0))) (\lambda (x:
+T).(\lambda (H3: (subst0 i0 u0 u1 x)).(\lambda (H4: (pr0 u3 x)).(ex_intro2 T
+(\lambda (t0: T).(subst0 i0 u0 (THead k u1 t) t0)) (\lambda (t0: T).(pr0
+(THead k u3 t) t0)) (THead k x t) (subst0_fst u0 x u1 i0 H3 t k) (pr0_comp u3
+x H4 t t (pr0_refl t) k))))) (H1 u0 H2)))))))))))) (\lambda (k: K).(\lambda
+(v: T).(\lambda (t3: T).(\lambda (t4: T).(\lambda (i0: nat).(\lambda (_:
+(subst0 (s k i0) v t4 t3)).(\lambda (H1: ((\forall (u1: T).((pr0 v u1) \to
+(ex2 T (\lambda (t: T).(subst0 (s k i0) u1 t4 t)) (\lambda (t: T).(pr0 t3
t))))))).(\lambda (u: T).(\lambda (u1: T).(\lambda (H2: (pr0 v u1)).(ex2_ind
-T (\lambda (t: T).(subst0 (s k i0) u1 t3 t)) (\lambda (t: T).(pr0 t0 t)) (ex2
-T (\lambda (t: T).(subst0 i0 u1 (THead k u t3) t)) (\lambda (t: T).(pr0
-(THead k u t0) t))) (\lambda (x: T).(\lambda (H3: (subst0 (s k i0) u1 t3
-x)).(\lambda (H4: (pr0 t0 x)).(ex_intro2 T (\lambda (t: T).(subst0 i0 u1
-(THead k u t3) t)) (\lambda (t: T).(pr0 (THead k u t0) t)) (THead k u x)
-(subst0_snd k u1 x t3 i0 H3 u) (pr0_comp u u (pr0_refl u) t0 x H4 k))))) (H1
-u1 H2)))))))))))) (\lambda (v: T).(\lambda (u1: T).(\lambda (u0: T).(\lambda
-(i0: nat).(\lambda (_: (subst0 i0 v u1 u0)).(\lambda (H1: ((\forall (u3:
-T).((pr0 v u3) \to (ex2 T (\lambda (t: T).(subst0 i0 u3 u1 t)) (\lambda (t:
-T).(pr0 u0 t))))))).(\lambda (k: K).(\lambda (t0: T).(\lambda (t3:
-T).(\lambda (_: (subst0 (s k i0) v t0 t3)).(\lambda (H3: ((\forall (u3:
-T).((pr0 v u3) \to (ex2 T (\lambda (t: T).(subst0 (s k i0) u3 t0 t)) (\lambda
-(t: T).(pr0 t3 t))))))).(\lambda (u3: T).(\lambda (H4: (pr0 v u3)).(ex2_ind T
-(\lambda (t: T).(subst0 (s k i0) u3 t0 t)) (\lambda (t: T).(pr0 t3 t)) (ex2 T
-(\lambda (t: T).(subst0 i0 u3 (THead k u1 t0) t)) (\lambda (t: T).(pr0 (THead
-k u0 t3) t))) (\lambda (x: T).(\lambda (H5: (subst0 (s k i0) u3 t0
-x)).(\lambda (H6: (pr0 t3 x)).(ex2_ind T (\lambda (t: T).(subst0 i0 u3 u1 t))
-(\lambda (t: T).(pr0 u0 t)) (ex2 T (\lambda (t: T).(subst0 i0 u3 (THead k u1
-t0) t)) (\lambda (t: T).(pr0 (THead k u0 t3) t))) (\lambda (x0: T).(\lambda
-(H7: (subst0 i0 u3 u1 x0)).(\lambda (H8: (pr0 u0 x0)).(ex_intro2 T (\lambda
-(t: T).(subst0 i0 u3 (THead k u1 t0) t)) (\lambda (t: T).(pr0 (THead k u0 t3)
-t)) (THead k x0 x) (subst0_both u3 u1 x0 i0 H7 k t0 x H5) (pr0_comp u0 x0 H8
-t3 x H6 k))))) (H1 u3 H4))))) (H3 u3 H4))))))))))))))) i u2 t1 t2 H))))).
+T (\lambda (t: T).(subst0 (s k i0) u1 t4 t)) (\lambda (t: T).(pr0 t3 t)) (ex2
+T (\lambda (t: T).(subst0 i0 u1 (THead k u t4) t)) (\lambda (t: T).(pr0
+(THead k u t3) t))) (\lambda (x: T).(\lambda (H3: (subst0 (s k i0) u1 t4
+x)).(\lambda (H4: (pr0 t3 x)).(ex_intro2 T (\lambda (t: T).(subst0 i0 u1
+(THead k u t4) t)) (\lambda (t: T).(pr0 (THead k u t3) t)) (THead k u x)
+(subst0_snd k u1 x t4 i0 H3 u) (pr0_comp u u (pr0_refl u) t3 x H4 k))))) (H1
+u1 H2)))))))))))) (\lambda (v: T).(\lambda (u1: T).(\lambda (u3: T).(\lambda
+(i0: nat).(\lambda (_: (subst0 i0 v u1 u3)).(\lambda (H1: ((\forall (u4:
+T).((pr0 v u4) \to (ex2 T (\lambda (t: T).(subst0 i0 u4 u1 t)) (\lambda (t:
+T).(pr0 u3 t))))))).(\lambda (k: K).(\lambda (t3: T).(\lambda (t4:
+T).(\lambda (_: (subst0 (s k i0) v t3 t4)).(\lambda (H3: ((\forall (u4:
+T).((pr0 v u4) \to (ex2 T (\lambda (t: T).(subst0 (s k i0) u4 t3 t)) (\lambda
+(t: T).(pr0 t4 t))))))).(\lambda (u0: T).(\lambda (H4: (pr0 v u0)).(ex2_ind T
+(\lambda (t: T).(subst0 (s k i0) u0 t3 t)) (\lambda (t: T).(pr0 t4 t)) (ex2 T
+(\lambda (t: T).(subst0 i0 u0 (THead k u1 t3) t)) (\lambda (t: T).(pr0 (THead
+k u3 t4) t))) (\lambda (x: T).(\lambda (H5: (subst0 (s k i0) u0 t3
+x)).(\lambda (H6: (pr0 t4 x)).(ex2_ind T (\lambda (t: T).(subst0 i0 u0 u1 t))
+(\lambda (t: T).(pr0 u3 t)) (ex2 T (\lambda (t: T).(subst0 i0 u0 (THead k u1
+t3) t)) (\lambda (t: T).(pr0 (THead k u3 t4) t))) (\lambda (x0: T).(\lambda
+(H7: (subst0 i0 u0 u1 x0)).(\lambda (H8: (pr0 u3 x0)).(ex_intro2 T (\lambda
+(t: T).(subst0 i0 u0 (THead k u1 t3) t)) (\lambda (t: T).(pr0 (THead k u3 t4)
+t)) (THead k x0 x) (subst0_both u0 u1 x0 i0 H7 k t3 x H5) (pr0_comp u3 x0 H8
+t4 x H6 k))))) (H1 u0 H4))))) (H3 u0 H4))))))))))))))) i u2 t1 t2 H))))).
theorem pr0_subst0:
\forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (v1: T).(\forall
Appl) i) v0 u u2)) (or (pr0 w1 (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda
(w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4)
w2)))) (\lambda (x0: T).(\lambda (H10: (eq T x (THead (Bind Abst) x0
-t3))).(\lambda (_: (subst0 (s (Flat Appl) i) v0 u x0)).(eq_ind_r T (THead
-(Flat Appl) v1 x) (\lambda (t: T).(or (pr0 t (THead (Bind Abbr) v2 t4)) (ex2
-T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
-Abbr) v2 t4) w2))))) (eq_ind_r T (THead (Bind Abst) x0 t3) (\lambda (t:
-T).(or (pr0 (THead (Flat Appl) v1 t) (THead (Bind Abbr) v2 t4)) (ex2 T
-(\lambda (w2: T).(pr0 (THead (Flat Appl) v1 t) w2)) (\lambda (w2: T).(subst0
-i v3 (THead (Bind Abbr) v2 t4) w2))))) (or_introl (pr0 (THead (Flat Appl) v1
-(THead (Bind Abst) x0 t3)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2:
-T).(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) x0 t3)) w2)) (\lambda (w2:
-T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))) (pr0_beta x0 v1 v2 H0 t3 t4
-H2)) x H10) w1 H7)))) H9)) (\lambda (H9: (ex2 T (\lambda (t5: T).(eq T x
-(THead (Bind Abst) u t5))) (\lambda (t5: T).(subst0 (s (Bind Abst) (s (Flat
-Appl) i)) v0 t3 t5)))).(ex2_ind T (\lambda (t5: T).(eq T x (THead (Bind Abst)
-u t5))) (\lambda (t5: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0 t3 t5))
-(or (pr0 w1 (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 w1 w2))
-(\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (x0:
-T).(\lambda (H10: (eq T x (THead (Bind Abst) u x0))).(\lambda (H11: (subst0
-(s (Bind Abst) (s (Flat Appl) i)) v0 t3 x0)).(eq_ind_r T (THead (Flat Appl)
-v1 x) (\lambda (t: T).(or (pr0 t (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda
-(w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4)
-w2))))) (eq_ind_r T (THead (Bind Abst) u x0) (\lambda (t: T).(or (pr0 (THead
-(Flat Appl) v1 t) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0
-(THead (Flat Appl) v1 t) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
-Abbr) v2 t4) w2))))) (or_ind (pr0 x0 t4) (ex2 T (\lambda (w2: T).(pr0 x0 w2))
-(\lambda (w2: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v3 t4 w2))) (or
-(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) u x0)) (THead (Bind Abbr) v2
-t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) u
-x0)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))))
-(\lambda (H12: (pr0 x0 t4)).(or_introl (pr0 (THead (Flat Appl) v1 (THead
-(Bind Abst) u x0)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0
-(THead (Flat Appl) v1 (THead (Bind Abst) u x0)) w2)) (\lambda (w2: T).(subst0
-i v3 (THead (Bind Abbr) v2 t4) w2))) (pr0_beta u v1 v2 H0 x0 t4 H12)))
-(\lambda (H12: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0
-(s (Bind Abst) (s (Flat Appl) i)) v3 t4 w2)))).(ex2_ind T (\lambda (w2:
+t3))).(\lambda (_: (subst0 (s (Flat Appl) i) v0 u x0)).(let H12 \def (eq_ind
+T x (\lambda (t: T).(eq T w1 (THead (Flat Appl) v1 t))) H7 (THead (Bind Abst)
+x0 t3) H10) in (eq_ind_r T (THead (Flat Appl) v1 (THead (Bind Abst) x0 t3))
+(\lambda (t: T).(or (pr0 t (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2:
+T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4)
+w2))))) (or_introl (pr0 (THead (Flat Appl) v1 (THead (Bind Abst) x0 t3))
+(THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1
+(THead (Bind Abst) x0 t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
+Abbr) v2 t4) w2))) (pr0_beta x0 v1 v2 H0 t3 t4 H2)) w1 H12))))) H9)) (\lambda
+(H9: (ex2 T (\lambda (t5: T).(eq T x (THead (Bind Abst) u t5))) (\lambda (t5:
+T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0 t3 t5)))).(ex2_ind T (\lambda
+(t5: T).(eq T x (THead (Bind Abst) u t5))) (\lambda (t5: T).(subst0 (s (Bind
+Abst) (s (Flat Appl) i)) v0 t3 t5)) (or (pr0 w1 (THead (Bind Abbr) v2 t4))
+(ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v3 (THead
+(Bind Abbr) v2 t4) w2)))) (\lambda (x0: T).(\lambda (H10: (eq T x (THead
+(Bind Abst) u x0))).(\lambda (H11: (subst0 (s (Bind Abst) (s (Flat Appl) i))
+v0 t3 x0)).(let H12 \def (eq_ind T x (\lambda (t: T).(eq T w1 (THead (Flat
+Appl) v1 t))) H7 (THead (Bind Abst) u x0) H10) in (eq_ind_r T (THead (Flat
+Appl) v1 (THead (Bind Abst) u x0)) (\lambda (t: T).(or (pr0 t (THead (Bind
+Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i
+v3 (THead (Bind Abbr) v2 t4) w2))))) (or_ind (pr0 x0 t4) (ex2 T (\lambda (w2:
T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v3
-t4 w2)) (or (pr0 (THead (Flat Appl) v1 (THead (Bind Abst) u x0)) (THead (Bind
-Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind
-Abst) u x0)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4)
-w2)))) (\lambda (x1: T).(\lambda (H13: (pr0 x0 x1)).(\lambda (H14: (subst0 (s
-(Bind Abst) (s (Flat Appl) i)) v3 t4 x1)).(or_intror (pr0 (THead (Flat Appl)
-v1 (THead (Bind Abst) u x0)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2:
-T).(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) u x0)) w2)) (\lambda (w2:
-T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))) (ex_intro2 T (\lambda (w2:
+t4 w2))) (or (pr0 (THead (Flat Appl) v1 (THead (Bind Abst) u x0)) (THead
+(Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead
+(Bind Abst) u x0)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2
+t4) w2)))) (\lambda (H13: (pr0 x0 t4)).(or_introl (pr0 (THead (Flat Appl) v1
+(THead (Bind Abst) u x0)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2:
T).(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) u x0)) w2)) (\lambda (w2:
-T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)) (THead (Bind Abbr) v2 x1)
-(pr0_beta u v1 v2 H0 x0 x1 H13) (subst0_snd (Bind Abbr) v3 x1 t4 i H14
-v2)))))) H12)) (H3 v0 x0 (s (Bind Abst) (s (Flat Appl) i)) H11 v3 H5)) x H10)
-w1 H7)))) H9)) (\lambda (H9: (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq
-T x (THead (Bind Abst) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(subst0 (s
-(Flat Appl) i) v0 u u2))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s (Bind
-Abst) (s (Flat Appl) i)) v0 t3 t5))))).(ex3_2_ind T T (\lambda (u2:
-T).(\lambda (t5: T).(eq T x (THead (Bind Abst) u2 t5)))) (\lambda (u2:
-T).(\lambda (_: T).(subst0 (s (Flat Appl) i) v0 u u2))) (\lambda (_:
-T).(\lambda (t5: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0 t3 t5))) (or
-(pr0 w1 (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 w1 w2))
-(\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (x0:
-T).(\lambda (x1: T).(\lambda (H10: (eq T x (THead (Bind Abst) x0
-x1))).(\lambda (_: (subst0 (s (Flat Appl) i) v0 u x0)).(\lambda (H12: (subst0
-(s (Bind Abst) (s (Flat Appl) i)) v0 t3 x1)).(eq_ind_r T (THead (Flat Appl)
-v1 x) (\lambda (t: T).(or (pr0 t (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda
-(w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4)
-w2))))) (eq_ind_r T (THead (Bind Abst) x0 x1) (\lambda (t: T).(or (pr0 (THead
-(Flat Appl) v1 t) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0
-(THead (Flat Appl) v1 t) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
-Abbr) v2 t4) w2))))) (or_ind (pr0 x1 t4) (ex2 T (\lambda (w2: T).(pr0 x1 w2))
-(\lambda (w2: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v3 t4 w2))) (or
-(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) x0 x1)) (THead (Bind Abbr) v2
-t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) x0
-x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))))
-(\lambda (H13: (pr0 x1 t4)).(or_introl (pr0 (THead (Flat Appl) v1 (THead
-(Bind Abst) x0 x1)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0
-(THead (Flat Appl) v1 (THead (Bind Abst) x0 x1)) w2)) (\lambda (w2:
-T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))) (pr0_beta x0 v1 v2 H0 x1 t4
-H13))) (\lambda (H13: (ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))) (pr0_beta u v1 v2 H0 x0 t4
+H13))) (\lambda (H13: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v3 t4 w2)))).(ex2_ind T (\lambda
-(w2: T).(pr0 x1 w2)) (\lambda (w2: T).(subst0 (s (Bind Abst) (s (Flat Appl)
-i)) v3 t4 w2)) (or (pr0 (THead (Flat Appl) v1 (THead (Bind Abst) x0 x1))
+(w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 (s (Bind Abst) (s (Flat Appl)
+i)) v3 t4 w2)) (or (pr0 (THead (Flat Appl) v1 (THead (Bind Abst) u x0))
(THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1
-(THead (Bind Abst) x0 x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
-Abbr) v2 t4) w2)))) (\lambda (x2: T).(\lambda (H14: (pr0 x1 x2)).(\lambda
-(H15: (subst0 (s (Bind Abst) (s (Flat Appl) i)) v3 t4 x2)).(or_intror (pr0
-(THead (Flat Appl) v1 (THead (Bind Abst) x0 x1)) (THead (Bind Abbr) v2 t4))
-(ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) x0 x1))
+(THead (Bind Abst) u x0)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
+Abbr) v2 t4) w2)))) (\lambda (x1: T).(\lambda (H14: (pr0 x0 x1)).(\lambda
+(H15: (subst0 (s (Bind Abst) (s (Flat Appl) i)) v3 t4 x1)).(or_intror (pr0
+(THead (Flat Appl) v1 (THead (Bind Abst) u x0)) (THead (Bind Abbr) v2 t4))
+(ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) u x0))
w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))) (ex_intro2
-T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) x0 x1)) w2))
+T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) u x0)) w2))
(\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)) (THead (Bind
-Abbr) v2 x2) (pr0_beta x0 v1 v2 H0 x1 x2 H14) (subst0_snd (Bind Abbr) v3 x2
-t4 i H15 v2)))))) H13)) (H3 v0 x1 (s (Bind Abst) (s (Flat Appl) i)) H12 v3
-H5)) x H10) w1 H7)))))) H9)) (subst0_gen_head (Bind Abst) v0 u t3 x (s (Flat
-Appl) i) H8))))) H6)) (\lambda (H6: (ex3_2 T T (\lambda (u2: T).(\lambda (t5:
+Abbr) v2 x1) (pr0_beta u v1 v2 H0 x0 x1 H14) (subst0_snd (Bind Abbr) v3 x1 t4
+i H15 v2)))))) H13)) (H3 v0 x0 (s (Bind Abst) (s (Flat Appl) i)) H11 v3 H5))
+w1 H12))))) H9)) (\lambda (H9: (ex3_2 T T (\lambda (u2: T).(\lambda (t5:
+T).(eq T x (THead (Bind Abst) u2 t5)))) (\lambda (u2: T).(\lambda (_:
+T).(subst0 (s (Flat Appl) i) v0 u u2))) (\lambda (_: T).(\lambda (t5:
+T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0 t3 t5))))).(ex3_2_ind T T
+(\lambda (u2: T).(\lambda (t5: T).(eq T x (THead (Bind Abst) u2 t5))))
+(\lambda (u2: T).(\lambda (_: T).(subst0 (s (Flat Appl) i) v0 u u2)))
+(\lambda (_: T).(\lambda (t5: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0
+t3 t5))) (or (pr0 w1 (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0
+w1 w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))))
+(\lambda (x0: T).(\lambda (x1: T).(\lambda (H10: (eq T x (THead (Bind Abst)
+x0 x1))).(\lambda (_: (subst0 (s (Flat Appl) i) v0 u x0)).(\lambda (H12:
+(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0 t3 x1)).(let H13 \def (eq_ind T
+x (\lambda (t: T).(eq T w1 (THead (Flat Appl) v1 t))) H7 (THead (Bind Abst)
+x0 x1) H10) in (eq_ind_r T (THead (Flat Appl) v1 (THead (Bind Abst) x0 x1))
+(\lambda (t: T).(or (pr0 t (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2:
+T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4)
+w2))))) (or_ind (pr0 x1 t4) (ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda
+(w2: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v3 t4 w2))) (or (pr0 (THead
+(Flat Appl) v1 (THead (Bind Abst) x0 x1)) (THead (Bind Abbr) v2 t4)) (ex2 T
+(\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) x0 x1)) w2))
+(\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (H14:
+(pr0 x1 t4)).(or_introl (pr0 (THead (Flat Appl) v1 (THead (Bind Abst) x0 x1))
+(THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1
+(THead (Bind Abst) x0 x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
+Abbr) v2 t4) w2))) (pr0_beta x0 v1 v2 H0 x1 t4 H14))) (\lambda (H14: (ex2 T
+(\lambda (w2: T).(pr0 x1 w2)) (\lambda (w2: T).(subst0 (s (Bind Abst) (s
+(Flat Appl) i)) v3 t4 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x1 w2))
+(\lambda (w2: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v3 t4 w2)) (or
+(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) x0 x1)) (THead (Bind Abbr) v2
+t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) x0
+x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))))
+(\lambda (x2: T).(\lambda (H15: (pr0 x1 x2)).(\lambda (H16: (subst0 (s (Bind
+Abst) (s (Flat Appl) i)) v3 t4 x2)).(or_intror (pr0 (THead (Flat Appl) v1
+(THead (Bind Abst) x0 x1)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2:
+T).(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) x0 x1)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))) (ex_intro2 T (\lambda (w2:
+T).(pr0 (THead (Flat Appl) v1 (THead (Bind Abst) x0 x1)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)) (THead (Bind Abbr) v2 x2)
+(pr0_beta x0 v1 v2 H0 x1 x2 H15) (subst0_snd (Bind Abbr) v3 x2 t4 i H16
+v2)))))) H14)) (H3 v0 x1 (s (Bind Abst) (s (Flat Appl) i)) H12 v3 H5)) w1
+H13))))))) H9)) (subst0_gen_head (Bind Abst) v0 u t3 x (s (Flat Appl) i)
+H8))))) H6)) (\lambda (H6: (ex3_2 T T (\lambda (u2: T).(\lambda (t5: T).(eq T
+w1 (THead (Flat Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_: T).(subst0 i v0
+v1 u2))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s (Flat Appl) i) v0 (THead
+(Bind Abst) u t3) t5))))).(ex3_2_ind T T (\lambda (u2: T).(\lambda (t5:
T).(eq T w1 (THead (Flat Appl) u2 t5)))) (\lambda (u2: T).(\lambda (_:
T).(subst0 i v0 v1 u2))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s (Flat
-Appl) i) v0 (THead (Bind Abst) u t3) t5))))).(ex3_2_ind T T (\lambda (u2:
-T).(\lambda (t5: T).(eq T w1 (THead (Flat Appl) u2 t5)))) (\lambda (u2:
-T).(\lambda (_: T).(subst0 i v0 v1 u2))) (\lambda (_: T).(\lambda (t5:
-T).(subst0 (s (Flat Appl) i) v0 (THead (Bind Abst) u t3) t5))) (or (pr0 w1
-(THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2:
-T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (x0: T).(\lambda
-(x1: T).(\lambda (H7: (eq T w1 (THead (Flat Appl) x0 x1))).(\lambda (H8:
-(subst0 i v0 v1 x0)).(\lambda (H9: (subst0 (s (Flat Appl) i) v0 (THead (Bind
-Abst) u t3) x1)).(or3_ind (ex2 T (\lambda (u2: T).(eq T x1 (THead (Bind Abst)
-u2 t3))) (\lambda (u2: T).(subst0 (s (Flat Appl) i) v0 u u2))) (ex2 T
-(\lambda (t5: T).(eq T x1 (THead (Bind Abst) u t5))) (\lambda (t5: T).(subst0
-(s (Bind Abst) (s (Flat Appl) i)) v0 t3 t5))) (ex3_2 T T (\lambda (u2:
-T).(\lambda (t5: T).(eq T x1 (THead (Bind Abst) u2 t5)))) (\lambda (u2:
-T).(\lambda (_: T).(subst0 (s (Flat Appl) i) v0 u u2))) (\lambda (_:
-T).(\lambda (t5: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0 t3 t5))))
-(or (pr0 w1 (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 w1 w2))
-(\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (H10:
-(ex2 T (\lambda (u2: T).(eq T x1 (THead (Bind Abst) u2 t3))) (\lambda (u2:
+Appl) i) v0 (THead (Bind Abst) u t3) t5))) (or (pr0 w1 (THead (Bind Abbr) v2
+t4)) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v3
+(THead (Bind Abbr) v2 t4) w2)))) (\lambda (x0: T).(\lambda (x1: T).(\lambda
+(H7: (eq T w1 (THead (Flat Appl) x0 x1))).(\lambda (H8: (subst0 i v0 v1
+x0)).(\lambda (H9: (subst0 (s (Flat Appl) i) v0 (THead (Bind Abst) u t3)
+x1)).(or3_ind (ex2 T (\lambda (u2: T).(eq T x1 (THead (Bind Abst) u2 t3)))
+(\lambda (u2: T).(subst0 (s (Flat Appl) i) v0 u u2))) (ex2 T (\lambda (t5:
+T).(eq T x1 (THead (Bind Abst) u t5))) (\lambda (t5: T).(subst0 (s (Bind
+Abst) (s (Flat Appl) i)) v0 t3 t5))) (ex3_2 T T (\lambda (u2: T).(\lambda
+(t5: T).(eq T x1 (THead (Bind Abst) u2 t5)))) (\lambda (u2: T).(\lambda (_:
+T).(subst0 (s (Flat Appl) i) v0 u u2))) (\lambda (_: T).(\lambda (t5:
+T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0 t3 t5)))) (or (pr0 w1 (THead
+(Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (H10: (ex2 T
+(\lambda (u2: T).(eq T x1 (THead (Bind Abst) u2 t3))) (\lambda (u2:
T).(subst0 (s (Flat Appl) i) v0 u u2)))).(ex2_ind T (\lambda (u2: T).(eq T x1
(THead (Bind Abst) u2 t3))) (\lambda (u2: T).(subst0 (s (Flat Appl) i) v0 u
u2)) (or (pr0 w1 (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 w1
w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda
(x: T).(\lambda (H11: (eq T x1 (THead (Bind Abst) x t3))).(\lambda (_:
-(subst0 (s (Flat Appl) i) v0 u x)).(eq_ind_r T (THead (Flat Appl) x0 x1)
-(\lambda (t: T).(or (pr0 t (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2:
-T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4)
-w2))))) (eq_ind_r T (THead (Bind Abst) x t3) (\lambda (t: T).(or (pr0 (THead
-(Flat Appl) x0 t) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0
-(THead (Flat Appl) x0 t) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
-Abbr) v2 t4) w2))))) (or_ind (pr0 x0 v2) (ex2 T (\lambda (w2: T).(pr0 x0 w2))
-(\lambda (w2: T).(subst0 i v3 v2 w2))) (or (pr0 (THead (Flat Appl) x0 (THead
-(Bind Abst) x t3)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0
-(THead (Flat Appl) x0 (THead (Bind Abst) x t3)) w2)) (\lambda (w2: T).(subst0
-i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (H13: (pr0 x0 v2)).(or_introl
-(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x t3)) (THead (Bind Abbr) v2
-t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x
-t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))
-(pr0_beta x x0 v2 H13 t3 t4 H2))) (\lambda (H13: (ex2 T (\lambda (w2: T).(pr0
-x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2)))).(ex2_ind T (\lambda (w2:
-T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2)) (or (pr0 (THead (Flat
-Appl) x0 (THead (Bind Abst) x t3)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda
-(w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x t3)) w2)) (\lambda
-(w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (x2:
-T).(\lambda (H14: (pr0 x0 x2)).(\lambda (H15: (subst0 i v3 v2 x2)).(or_intror
-(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x t3)) (THead (Bind Abbr) v2
-t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x
-t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))
-(ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x
-t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)) (THead
-(Bind Abbr) x2 t4) (pr0_beta x x0 x2 H14 t3 t4 H2) (subst0_fst v3 x2 v2 i H15
-t4 (Bind Abbr))))))) H13)) (H1 v0 x0 i H8 v3 H5)) x1 H11) w1 H7)))) H10))
-(\lambda (H10: (ex2 T (\lambda (t5: T).(eq T x1 (THead (Bind Abst) u t5)))
-(\lambda (t5: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0 t3
-t5)))).(ex2_ind T (\lambda (t5: T).(eq T x1 (THead (Bind Abst) u t5)))
-(\lambda (t5: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0 t3 t5)) (or
-(pr0 w1 (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 w1 w2))
-(\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (x:
-T).(\lambda (H11: (eq T x1 (THead (Bind Abst) u x))).(\lambda (H12: (subst0
-(s (Bind Abst) (s (Flat Appl) i)) v0 t3 x)).(eq_ind_r T (THead (Flat Appl) x0
-x1) (\lambda (t: T).(or (pr0 t (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda
-(w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4)
-w2))))) (eq_ind_r T (THead (Bind Abst) u x) (\lambda (t: T).(or (pr0 (THead
-(Flat Appl) x0 t) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0
-(THead (Flat Appl) x0 t) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
-Abbr) v2 t4) w2))))) (or_ind (pr0 x t4) (ex2 T (\lambda (w2: T).(pr0 x w2))
-(\lambda (w2: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v3 t4 w2))) (or
-(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) u x)) (THead (Bind Abbr) v2
-t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) u
-x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))))
-(\lambda (H13: (pr0 x t4)).(or_ind (pr0 x0 v2) (ex2 T (\lambda (w2: T).(pr0
-x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2))) (or (pr0 (THead (Flat Appl) x0
-(THead (Bind Abst) u x)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2:
-T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) u x)) w2)) (\lambda (w2:
-T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (H14: (pr0 x0
+(subst0 (s (Flat Appl) i) v0 u x)).(let H13 \def (eq_ind T x1 (\lambda (t:
+T).(eq T w1 (THead (Flat Appl) x0 t))) H7 (THead (Bind Abst) x t3) H11) in
+(eq_ind_r T (THead (Flat Appl) x0 (THead (Bind Abst) x t3)) (\lambda (t:
+T).(or (pr0 t (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 t w2))
+(\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))))) (or_ind (pr0
+x0 v2) (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2
+w2))) (or (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x t3)) (THead (Bind
+Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind
+Abst) x t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4)
+w2)))) (\lambda (H14: (pr0 x0 v2)).(or_introl (pr0 (THead (Flat Appl) x0
+(THead (Bind Abst) x t3)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2:
+T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x t3)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))) (pr0_beta x x0 v2 H14 t3 t4
+H2))) (\lambda (H14: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
+T).(subst0 i v3 v2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda
+(w2: T).(subst0 i v3 v2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind
+Abst) x t3)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead
+(Flat Appl) x0 (THead (Bind Abst) x t3)) w2)) (\lambda (w2: T).(subst0 i v3
+(THead (Bind Abbr) v2 t4) w2)))) (\lambda (x2: T).(\lambda (H15: (pr0 x0
+x2)).(\lambda (H16: (subst0 i v3 v2 x2)).(or_intror (pr0 (THead (Flat Appl)
+x0 (THead (Bind Abst) x t3)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2:
+T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x t3)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))) (ex_intro2 T (\lambda (w2:
+T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x t3)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)) (THead (Bind Abbr) x2 t4)
+(pr0_beta x x0 x2 H15 t3 t4 H2) (subst0_fst v3 x2 v2 i H16 t4 (Bind
+Abbr))))))) H14)) (H1 v0 x0 i H8 v3 H5)) w1 H13))))) H10)) (\lambda (H10:
+(ex2 T (\lambda (t5: T).(eq T x1 (THead (Bind Abst) u t5))) (\lambda (t5:
+T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0 t3 t5)))).(ex2_ind T (\lambda
+(t5: T).(eq T x1 (THead (Bind Abst) u t5))) (\lambda (t5: T).(subst0 (s (Bind
+Abst) (s (Flat Appl) i)) v0 t3 t5)) (or (pr0 w1 (THead (Bind Abbr) v2 t4))
+(ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v3 (THead
+(Bind Abbr) v2 t4) w2)))) (\lambda (x: T).(\lambda (H11: (eq T x1 (THead
+(Bind Abst) u x))).(\lambda (H12: (subst0 (s (Bind Abst) (s (Flat Appl) i))
+v0 t3 x)).(let H13 \def (eq_ind T x1 (\lambda (t: T).(eq T w1 (THead (Flat
+Appl) x0 t))) H7 (THead (Bind Abst) u x) H11) in (eq_ind_r T (THead (Flat
+Appl) x0 (THead (Bind Abst) u x)) (\lambda (t: T).(or (pr0 t (THead (Bind
+Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i
+v3 (THead (Bind Abbr) v2 t4) w2))))) (or_ind (pr0 x t4) (ex2 T (\lambda (w2:
+T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v3
+t4 w2))) (or (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) u x)) (THead (Bind
+Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind
+Abst) u x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4)
+w2)))) (\lambda (H14: (pr0 x t4)).(or_ind (pr0 x0 v2) (ex2 T (\lambda (w2:
+T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2))) (or (pr0 (THead (Flat
+Appl) x0 (THead (Bind Abst) u x)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda
+(w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) u x)) w2)) (\lambda
+(w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (H15: (pr0 x0
v2)).(or_introl (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) u x)) (THead
(Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
(Bind Abst) u x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2
-t4) w2))) (pr0_beta u x0 v2 H14 x t4 H13))) (\lambda (H14: (ex2 T (\lambda
+t4) w2))) (pr0_beta u x0 v2 H15 x t4 H14))) (\lambda (H15: (ex2 T (\lambda
(w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2)))).(ex2_ind T
(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2)) (or (pr0
(THead (Flat Appl) x0 (THead (Bind Abst) u x)) (THead (Bind Abbr) v2 t4))
(ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) u x))
w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda
-(x2: T).(\lambda (H15: (pr0 x0 x2)).(\lambda (H16: (subst0 i v3 v2
+(x2: T).(\lambda (H16: (pr0 x0 x2)).(\lambda (H17: (subst0 i v3 v2
x2)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) u x)) (THead
(Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
(Bind Abst) u x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2
t4) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
(Bind Abst) u x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2
-t4) w2)) (THead (Bind Abbr) x2 t4) (pr0_beta u x0 x2 H15 x t4 H13)
-(subst0_fst v3 x2 v2 i H16 t4 (Bind Abbr))))))) H14)) (H1 v0 x0 i H8 v3 H5)))
-(\lambda (H13: (ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0
+t4) w2)) (THead (Bind Abbr) x2 t4) (pr0_beta u x0 x2 H16 x t4 H14)
+(subst0_fst v3 x2 v2 i H17 t4 (Bind Abbr))))))) H15)) (H1 v0 x0 i H8 v3 H5)))
+(\lambda (H14: (ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0
(s (Bind Abst) (s (Flat Appl) i)) v3 t4 w2)))).(ex2_ind T (\lambda (w2:
T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v3
t4 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) u x)) (THead (Bind
Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind
Abst) u x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4)
-w2)))) (\lambda (x2: T).(\lambda (H14: (pr0 x x2)).(\lambda (H15: (subst0 (s
+w2)))) (\lambda (x2: T).(\lambda (H15: (pr0 x x2)).(\lambda (H16: (subst0 (s
(Bind Abst) (s (Flat Appl) i)) v3 t4 x2)).(or_ind (pr0 x0 v2) (ex2 T (\lambda
(w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2))) (or (pr0 (THead
(Flat Appl) x0 (THead (Bind Abst) u x)) (THead (Bind Abbr) v2 t4)) (ex2 T
(\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) u x)) w2))
-(\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (H16:
+(\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (H17:
(pr0 x0 v2)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) u x))
(THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0
(THead (Bind Abst) u x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
Abbr) v2 t4) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0
(THead (Bind Abst) u x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
-Abbr) v2 t4) w2)) (THead (Bind Abbr) v2 x2) (pr0_beta u x0 v2 H16 x x2 H14)
-(subst0_snd (Bind Abbr) v3 x2 t4 i H15 v2)))) (\lambda (H16: (ex2 T (\lambda
+Abbr) v2 t4) w2)) (THead (Bind Abbr) v2 x2) (pr0_beta u x0 v2 H17 x x2 H15)
+(subst0_snd (Bind Abbr) v3 x2 t4 i H16 v2)))) (\lambda (H17: (ex2 T (\lambda
(w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2)))).(ex2_ind T
(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2)) (or (pr0
(THead (Flat Appl) x0 (THead (Bind Abst) u x)) (THead (Bind Abbr) v2 t4))
(ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) u x))
w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda
-(x3: T).(\lambda (H17: (pr0 x0 x3)).(\lambda (H18: (subst0 i v3 v2
+(x3: T).(\lambda (H18: (pr0 x0 x3)).(\lambda (H19: (subst0 i v3 v2
x3)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) u x)) (THead
(Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
(Bind Abst) u x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2
t4) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
(Bind Abst) u x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2
-t4) w2)) (THead (Bind Abbr) x3 x2) (pr0_beta u x0 x3 H17 x x2 H14)
-(subst0_both v3 v2 x3 i H18 (Bind Abbr) t4 x2 H15)))))) H16)) (H1 v0 x0 i H8
-v3 H5))))) H13)) (H3 v0 x (s (Bind Abst) (s (Flat Appl) i)) H12 v3 H5)) x1
-H11) w1 H7)))) H10)) (\lambda (H10: (ex3_2 T T (\lambda (u2: T).(\lambda (t5:
+t4) w2)) (THead (Bind Abbr) x3 x2) (pr0_beta u x0 x3 H18 x x2 H15)
+(subst0_both v3 v2 x3 i H19 (Bind Abbr) t4 x2 H16)))))) H17)) (H1 v0 x0 i H8
+v3 H5))))) H14)) (H3 v0 x (s (Bind Abst) (s (Flat Appl) i)) H12 v3 H5)) w1
+H13))))) H10)) (\lambda (H10: (ex3_2 T T (\lambda (u2: T).(\lambda (t5:
T).(eq T x1 (THead (Bind Abst) u2 t5)))) (\lambda (u2: T).(\lambda (_:
T).(subst0 (s (Flat Appl) i) v0 u u2))) (\lambda (_: T).(\lambda (t5:
T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0 t3 t5))))).(ex3_2_ind T T
w1 w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))))
(\lambda (x2: T).(\lambda (x3: T).(\lambda (H11: (eq T x1 (THead (Bind Abst)
x2 x3))).(\lambda (_: (subst0 (s (Flat Appl) i) v0 u x2)).(\lambda (H13:
-(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0 t3 x3)).(eq_ind_r T (THead (Flat
-Appl) x0 x1) (\lambda (t: T).(or (pr0 t (THead (Bind Abbr) v2 t4)) (ex2 T
-(\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr)
-v2 t4) w2))))) (eq_ind_r T (THead (Bind Abst) x2 x3) (\lambda (t: T).(or (pr0
-(THead (Flat Appl) x0 t) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2:
-T).(pr0 (THead (Flat Appl) x0 t) w2)) (\lambda (w2: T).(subst0 i v3 (THead
-(Bind Abbr) v2 t4) w2))))) (or_ind (pr0 x3 t4) (ex2 T (\lambda (w2: T).(pr0
-x3 w2)) (\lambda (w2: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v3 t4
-w2))) (or (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x2 x3)) (THead (Bind
-Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind
-Abst) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4)
-w2)))) (\lambda (H14: (pr0 x3 t4)).(or_ind (pr0 x0 v2) (ex2 T (\lambda (w2:
-T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2))) (or (pr0 (THead (Flat
-Appl) x0 (THead (Bind Abst) x2 x3)) (THead (Bind Abbr) v2 t4)) (ex2 T
+(subst0 (s (Bind Abst) (s (Flat Appl) i)) v0 t3 x3)).(let H14 \def (eq_ind T
+x1 (\lambda (t: T).(eq T w1 (THead (Flat Appl) x0 t))) H7 (THead (Bind Abst)
+x2 x3) H11) in (eq_ind_r T (THead (Flat Appl) x0 (THead (Bind Abst) x2 x3))
+(\lambda (t: T).(or (pr0 t (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2:
+T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4)
+w2))))) (or_ind (pr0 x3 t4) (ex2 T (\lambda (w2: T).(pr0 x3 w2)) (\lambda
+(w2: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v3 t4 w2))) (or (pr0 (THead
+(Flat Appl) x0 (THead (Bind Abst) x2 x3)) (THead (Bind Abbr) v2 t4)) (ex2 T
(\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x2 x3)) w2))
(\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (H15:
-(pr0 x0 v2)).(or_introl (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x2 x3))
-(THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0
-(THead (Bind Abst) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
-Abbr) v2 t4) w2))) (pr0_beta x2 x0 v2 H15 x3 t4 H14))) (\lambda (H15: (ex2 T
-(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2
-w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3
-v2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x2 x3)) (THead
+(pr0 x3 t4)).(or_ind (pr0 x0 v2) (ex2 T (\lambda (w2: T).(pr0 x0 w2))
+(\lambda (w2: T).(subst0 i v3 v2 w2))) (or (pr0 (THead (Flat Appl) x0 (THead
+(Bind Abst) x2 x3)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0
+(THead (Flat Appl) x0 (THead (Bind Abst) x2 x3)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (H16: (pr0 x0
+v2)).(or_introl (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x2 x3)) (THead
(Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
(Bind Abst) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2
-t4) w2)))) (\lambda (x: T).(\lambda (H16: (pr0 x0 x)).(\lambda (H17: (subst0
-i v3 v2 x)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x2 x3))
-(THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0
-(THead (Bind Abst) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
-Abbr) v2 t4) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0
-(THead (Bind Abst) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind
-Abbr) v2 t4) w2)) (THead (Bind Abbr) x t4) (pr0_beta x2 x0 x H16 x3 t4 H14)
-(subst0_fst v3 x v2 i H17 t4 (Bind Abbr))))))) H15)) (H1 v0 x0 i H8 v3 H5)))
-(\lambda (H14: (ex2 T (\lambda (w2: T).(pr0 x3 w2)) (\lambda (w2: T).(subst0
+t4) w2))) (pr0_beta x2 x0 v2 H16 x3 t4 H15))) (\lambda (H16: (ex2 T (\lambda
+(w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2)))).(ex2_ind T
+(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2)) (or (pr0
+(THead (Flat Appl) x0 (THead (Bind Abst) x2 x3)) (THead (Bind Abbr) v2 t4))
+(ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x2 x3))
+w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda
+(x: T).(\lambda (H17: (pr0 x0 x)).(\lambda (H18: (subst0 i v3 v2
+x)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x2 x3)) (THead
+(Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
+(Bind Abst) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2
+t4) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
+(Bind Abst) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2
+t4) w2)) (THead (Bind Abbr) x t4) (pr0_beta x2 x0 x H17 x3 t4 H15)
+(subst0_fst v3 x v2 i H18 t4 (Bind Abbr))))))) H16)) (H1 v0 x0 i H8 v3 H5)))
+(\lambda (H15: (ex2 T (\lambda (w2: T).(pr0 x3 w2)) (\lambda (w2: T).(subst0
(s (Bind Abst) (s (Flat Appl) i)) v3 t4 w2)))).(ex2_ind T (\lambda (w2:
T).(pr0 x3 w2)) (\lambda (w2: T).(subst0 (s (Bind Abst) (s (Flat Appl) i)) v3
t4 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x2 x3)) (THead
(Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
(Bind Abst) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2
-t4) w2)))) (\lambda (x: T).(\lambda (H15: (pr0 x3 x)).(\lambda (H16: (subst0
+t4) w2)))) (\lambda (x: T).(\lambda (H16: (pr0 x3 x)).(\lambda (H17: (subst0
(s (Bind Abst) (s (Flat Appl) i)) v3 t4 x)).(or_ind (pr0 x0 v2) (ex2 T
(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2))) (or (pr0
(THead (Flat Appl) x0 (THead (Bind Abst) x2 x3)) (THead (Bind Abbr) v2 t4))
(ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x2 x3))
w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda
-(H17: (pr0 x0 v2)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind Abst)
+(H18: (pr0 x0 v2)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind Abst)
x2 x3)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat
Appl) x0 (THead (Bind Abst) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead
(Bind Abbr) v2 t4) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat
Appl) x0 (THead (Bind Abst) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead
-(Bind Abbr) v2 t4) w2)) (THead (Bind Abbr) v2 x) (pr0_beta x2 x0 v2 H17 x3 x
-H15) (subst0_snd (Bind Abbr) v3 x t4 i H16 v2)))) (\lambda (H17: (ex2 T
+(Bind Abbr) v2 t4) w2)) (THead (Bind Abbr) v2 x) (pr0_beta x2 x0 v2 H18 x3 x
+H16) (subst0_snd (Bind Abbr) v3 x t4 i H17 v2)))) (\lambda (H18: (ex2 T
(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2
w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3
v2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind Abst) x2 x3)) (THead
(Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
(Bind Abst) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2
-t4) w2)))) (\lambda (x4: T).(\lambda (H18: (pr0 x0 x4)).(\lambda (H19:
+t4) w2)))) (\lambda (x4: T).(\lambda (H19: (pr0 x0 x4)).(\lambda (H20:
(subst0 i v3 v2 x4)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind Abst)
x2 x3)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat
Appl) x0 (THead (Bind Abst) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead
(Bind Abbr) v2 t4) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat
Appl) x0 (THead (Bind Abst) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead
-(Bind Abbr) v2 t4) w2)) (THead (Bind Abbr) x4 x) (pr0_beta x2 x0 x4 H18 x3 x
-H15) (subst0_both v3 v2 x4 i H19 (Bind Abbr) t4 x H16)))))) H17)) (H1 v0 x0 i
-H8 v3 H5))))) H14)) (H3 v0 x3 (s (Bind Abst) (s (Flat Appl) i)) H13 v3 H5))
-x1 H11) w1 H7)))))) H10)) (subst0_gen_head (Bind Abst) v0 u t3 x1 (s (Flat
-Appl) i) H9))))))) H6)) (subst0_gen_head (Flat Appl) v0 v1 (THead (Bind Abst)
-u t3) w1 i H4))))))))))))))))) (\lambda (b: B).(\lambda (H0: (not (eq B b
+(Bind Abbr) v2 t4) w2)) (THead (Bind Abbr) x4 x) (pr0_beta x2 x0 x4 H19 x3 x
+H16) (subst0_both v3 v2 x4 i H20 (Bind Abbr) t4 x H17)))))) H18)) (H1 v0 x0 i
+H8 v3 H5))))) H15)) (H3 v0 x3 (s (Bind Abst) (s (Flat Appl) i)) H13 v3 H5))
+w1 H14))))))) H10)) (subst0_gen_head (Bind Abst) v0 u t3 x1 (s (Flat Appl) i)
+H9))))))) H6)) (subst0_gen_head (Flat Appl) v0 v1 (THead (Bind Abst) u t3) w1
+i H4))))))))))))))))) (\lambda (b: B).(\lambda (H0: (not (eq B b
Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (H1: (pr0 v1 v2)).(\lambda
(H2: ((\forall (v3: T).(\forall (w1: T).(\forall (i: nat).((subst0 i v3 v1
w1) \to (\forall (v4: T).((pr0 v3 v4) \to (or (pr0 w1 v2) (ex2 T (\lambda
(w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead
(Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (x0: T).(\lambda (H13: (eq
T x (THead (Bind b) x0 t3))).(\lambda (H14: (subst0 (s (Flat Appl) i) v0 u1
-x0)).(eq_ind_r T (THead (Flat Appl) v1 x) (\lambda (t: T).(or (pr0 t (THead
+x0)).(let H15 \def (eq_ind T x (\lambda (t: T).(eq T w1 (THead (Flat Appl) v1
+t))) H10 (THead (Bind b) x0 t3) H13) in (eq_ind_r T (THead (Flat Appl) v1
+(THead (Bind b) x0 t3)) (\lambda (t: T).(or (pr0 t (THead (Bind b) u2 (THead
+(Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 t w2))
+(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
+O) O v2) t4)) w2))))) (or_ind (pr0 x0 u2) (ex2 T (\lambda (w2: T).(pr0 x0
+w2)) (\lambda (w2: T).(subst0 (s (Flat Appl) i) v3 u2 w2))) (or (pr0 (THead
+(Flat Appl) v1 (THead (Bind b) x0 t3)) (THead (Bind b) u2 (THead (Flat Appl)
+(lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1
+(THead (Bind b) x0 t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2
+(THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H16: (pr0 x0
+u2)).(or_introl (pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 t3)) (THead
(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
-T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4)) w2))))) (eq_ind_r T (THead (Bind b) x0 t3)
-(\lambda (t: T).(or (pr0 (THead (Flat Appl) v1 t) (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat
-Appl) v1 t) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O v2) t4)) w2))))) (or_ind (pr0 x0 u2) (ex2 T
+T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 t3)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
+w2))) (pr0_upsilon b H0 v1 v2 H1 x0 u2 H16 t3 t4 H5))) (\lambda (H16: (ex2 T
(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 (s (Flat Appl) i) v3
-u2 w2))) (or (pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 t3)) (THead (Bind
-b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0
-(THead (Flat Appl) v1 (THead (Bind b) x0 t3)) w2)) (\lambda (w2: T).(subst0 i
-v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
-(\lambda (H15: (pr0 x0 u2)).(or_introl (pr0 (THead (Flat Appl) v1 (THead
-(Bind b) x0 t3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
-t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0
-t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
-(lift (S O) O v2) t4)) w2))) (pr0_upsilon b H0 v1 v2 H1 x0 u2 H15 t3 t4 H5)))
-(\lambda (H15: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0
-(s (Flat Appl) i) v3 u2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2))
-(\lambda (w2: T).(subst0 (s (Flat Appl) i) v3 u2 w2)) (or (pr0 (THead (Flat
-Appl) v1 (THead (Bind b) x0 t3)) (THead (Bind b) u2 (THead (Flat Appl) (lift
-(S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead
-(Bind b) x0 t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (x1: T).(\lambda (H16:
-(pr0 x0 x1)).(\lambda (H17: (subst0 (s (Flat Appl) i) v3 u2 x1)).(or_intror
-(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 t3)) (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat
-Appl) v1 (THead (Bind b) x0 t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead
-(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))) (ex_intro2 T
+u2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0
+(s (Flat Appl) i) v3 u2 w2)) (or (pr0 (THead (Flat Appl) v1 (THead (Bind b)
+x0 t3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
(\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 t3)) w2))
(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2)) (THead (Bind b) x1 (THead (Flat Appl) (lift (S O) O v2)
-t4)) (pr0_upsilon b H0 v1 v2 H1 x0 x1 H16 t3 t4 H5) (subst0_fst v3 x1 u2 i
-H17 (THead (Flat Appl) (lift (S O) O v2) t4) (Bind b))))))) H15)) (H4 v0 x0
-(s (Flat Appl) i) H14 v3 H8)) x H13) w1 H10)))) H12)) (\lambda (H12: (ex2 T
-(\lambda (t5: T).(eq T x (THead (Bind b) u1 t5))) (\lambda (t5: T).(subst0 (s
-(Bind b) (s (Flat Appl) i)) v0 t3 t5)))).(ex2_ind T (\lambda (t5: T).(eq T x
-(THead (Bind b) u1 t5))) (\lambda (t5: T).(subst0 (s (Bind b) (s (Flat Appl)
-i)) v0 t3 t5)) (or (pr0 w1 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O)
-O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i
-v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
-(\lambda (x0: T).(\lambda (H13: (eq T x (THead (Bind b) u1 x0))).(\lambda
-(H14: (subst0 (s (Bind b) (s (Flat Appl) i)) v0 t3 x0)).(eq_ind_r T (THead
-(Flat Appl) v1 x) (\lambda (t: T).(or (pr0 t (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda
-(w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
-t4)) w2))))) (eq_ind_r T (THead (Bind b) u1 x0) (\lambda (t: T).(or (pr0
-(THead (Flat Appl) v1 t) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
-v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 t) w2)) (\lambda
-(w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
-t4)) w2))))) (or_ind (pr0 x0 t4) (ex2 T (\lambda (w2: T).(pr0 x0 w2))
-(\lambda (w2: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4 w2))) (or (pr0
-(THead (Flat Appl) v1 (THead (Bind b) u1 x0)) (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl)
-v1 (THead (Bind b) u1 x0)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b)
-u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H15: (pr0 x0
-t4)).(or_introl (pr0 (THead (Flat Appl) v1 (THead (Bind b) u1 x0)) (THead
+O) O v2) t4)) w2)))) (\lambda (x1: T).(\lambda (H17: (pr0 x0 x1)).(\lambda
+(H18: (subst0 (s (Flat Appl) i) v3 u2 x1)).(or_intror (pr0 (THead (Flat Appl)
+v1 (THead (Bind b) x0 t3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O)
+O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind
+b) x0 t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
+Appl) (lift (S O) O v2) t4)) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead
+(Flat Appl) v1 (THead (Bind b) x0 t3)) w2)) (\lambda (w2: T).(subst0 i v3
+(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)) (THead
+(Bind b) x1 (THead (Flat Appl) (lift (S O) O v2) t4)) (pr0_upsilon b H0 v1 v2
+H1 x0 x1 H17 t3 t4 H5) (subst0_fst v3 x1 u2 i H18 (THead (Flat Appl) (lift (S
+O) O v2) t4) (Bind b))))))) H16)) (H4 v0 x0 (s (Flat Appl) i) H14 v3 H8)) w1
+H15))))) H12)) (\lambda (H12: (ex2 T (\lambda (t5: T).(eq T x (THead (Bind b)
+u1 t5))) (\lambda (t5: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v0 t3
+t5)))).(ex2_ind T (\lambda (t5: T).(eq T x (THead (Bind b) u1 t5))) (\lambda
+(t5: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v0 t3 t5)) (or (pr0 w1 (THead
(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
-T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) u1 x0)) w2)) (\lambda (w2:
-T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
-w2))) (pr0_upsilon b H0 v1 v2 H1 u1 u2 H3 x0 t4 H15))) (\lambda (H15: (ex2 T
-(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 (s (Bind b) (s (Flat
-Appl) i)) v3 t4 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
-T).(subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4 w2)) (or (pr0 (THead (Flat
-Appl) v1 (THead (Bind b) u1 x0)) (THead (Bind b) u2 (THead (Flat Appl) (lift
-(S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead
-(Bind b) u1 x0)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (x1: T).(\lambda (H16:
-(pr0 x0 x1)).(\lambda (H17: (subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4
-x1)).(or_intror (pr0 (THead (Flat Appl) v1 (THead (Bind b) u1 x0)) (THead
+T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
+Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (x0: T).(\lambda (H13: (eq T x
+(THead (Bind b) u1 x0))).(\lambda (H14: (subst0 (s (Bind b) (s (Flat Appl)
+i)) v0 t3 x0)).(let H15 \def (eq_ind T x (\lambda (t: T).(eq T w1 (THead
+(Flat Appl) v1 t))) H10 (THead (Bind b) u1 x0) H13) in (eq_ind_r T (THead
+(Flat Appl) v1 (THead (Bind b) u1 x0)) (\lambda (t: T).(or (pr0 t (THead
(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
-T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) u1 x0)) w2)) (\lambda (w2:
-T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
-w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind
-b) u1 x0)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) u2 (THead (Flat Appl) (lift
-(S O) O v2) x1)) (pr0_upsilon b H0 v1 v2 H1 u1 u2 H3 x0 x1 H16) (subst0_snd
-(Bind b) v3 (THead (Flat Appl) (lift (S O) O v2) x1) (THead (Flat Appl) (lift
-(S O) O v2) t4) i (subst0_snd (Flat Appl) v3 x1 t4 (s (Bind b) i) H17 (lift
-(S O) O v2)) u2)))))) H15)) (H6 v0 x0 (s (Bind b) (s (Flat Appl) i)) H14 v3
-H8)) x H13) w1 H10)))) H12)) (\lambda (H12: (ex3_2 T T (\lambda (u3:
-T).(\lambda (t5: T).(eq T x (THead (Bind b) u3 t5)))) (\lambda (u3:
-T).(\lambda (_: T).(subst0 (s (Flat Appl) i) v0 u1 u3))) (\lambda (_:
+T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
+Appl) (lift (S O) O v2) t4)) w2))))) (or_ind (pr0 x0 t4) (ex2 T (\lambda (w2:
+T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4
+w2))) (or (pr0 (THead (Flat Appl) v1 (THead (Bind b) u1 x0)) (THead (Bind b)
+u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0
+(THead (Flat Appl) v1 (THead (Bind b) u1 x0)) w2)) (\lambda (w2: T).(subst0 i
+v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
+(\lambda (H16: (pr0 x0 t4)).(or_introl (pr0 (THead (Flat Appl) v1 (THead
+(Bind b) u1 x0)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
+t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) u1
+x0)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
+(lift (S O) O v2) t4)) w2))) (pr0_upsilon b H0 v1 v2 H1 u1 u2 H3 x0 t4 H16)))
+(\lambda (H16: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0
+(s (Bind b) (s (Flat Appl) i)) v3 t4 w2)))).(ex2_ind T (\lambda (w2: T).(pr0
+x0 w2)) (\lambda (w2: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4 w2))
+(or (pr0 (THead (Flat Appl) v1 (THead (Bind b) u1 x0)) (THead (Bind b) u2
+(THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0
+(THead (Flat Appl) v1 (THead (Bind b) u1 x0)) w2)) (\lambda (w2: T).(subst0 i
+v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
+(\lambda (x1: T).(\lambda (H17: (pr0 x0 x1)).(\lambda (H18: (subst0 (s (Bind
+b) (s (Flat Appl) i)) v3 t4 x1)).(or_intror (pr0 (THead (Flat Appl) v1 (THead
+(Bind b) u1 x0)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
+t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) u1
+x0)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
+(lift (S O) O v2) t4)) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat
+Appl) v1 (THead (Bind b) u1 x0)) w2)) (\lambda (w2: T).(subst0 i v3 (THead
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) u2
+(THead (Flat Appl) (lift (S O) O v2) x1)) (pr0_upsilon b H0 v1 v2 H1 u1 u2 H3
+x0 x1 H17) (subst0_snd (Bind b) v3 (THead (Flat Appl) (lift (S O) O v2) x1)
+(THead (Flat Appl) (lift (S O) O v2) t4) i (subst0_snd (Flat Appl) v3 x1 t4
+(s (Bind b) i) H18 (lift (S O) O v2)) u2)))))) H16)) (H6 v0 x0 (s (Bind b) (s
+(Flat Appl) i)) H14 v3 H8)) w1 H15))))) H12)) (\lambda (H12: (ex3_2 T T
+(\lambda (u3: T).(\lambda (t5: T).(eq T x (THead (Bind b) u3 t5)))) (\lambda
+(u3: T).(\lambda (_: T).(subst0 (s (Flat Appl) i) v0 u1 u3))) (\lambda (_:
T).(\lambda (t5: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v0 t3
t5))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda (t5: T).(eq T x (THead (Bind
b) u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 (s (Flat Appl) i) v0 u1
(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda
(x0: T).(\lambda (x1: T).(\lambda (H13: (eq T x (THead (Bind b) x0
x1))).(\lambda (H14: (subst0 (s (Flat Appl) i) v0 u1 x0)).(\lambda (H15:
-(subst0 (s (Bind b) (s (Flat Appl) i)) v0 t3 x1)).(eq_ind_r T (THead (Flat
-Appl) v1 x) (\lambda (t: T).(or (pr0 t (THead (Bind b) u2 (THead (Flat Appl)
-(lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2:
+(subst0 (s (Bind b) (s (Flat Appl) i)) v0 t3 x1)).(let H16 \def (eq_ind T x
+(\lambda (t: T).(eq T w1 (THead (Flat Appl) v1 t))) H10 (THead (Bind b) x0
+x1) H13) in (eq_ind_r T (THead (Flat Appl) v1 (THead (Bind b) x0 x1))
+(\lambda (t: T).(or (pr0 t (THead (Bind b) u2 (THead (Flat Appl) (lift (S O)
+O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3
+(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))) (or_ind
+(pr0 x1 t4) (ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda (w2: T).(subst0 (s
+(Bind b) (s (Flat Appl) i)) v3 t4 w2))) (or (pr0 (THead (Flat Appl) v1 (THead
+(Bind b) x0 x1)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
+t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0
+x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
+(lift (S O) O v2) t4)) w2)))) (\lambda (H17: (pr0 x1 t4)).(or_ind (pr0 x0 u2)
+(ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 (s (Flat Appl)
+i) v3 u2 w2))) (or (pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 x1)) (THead
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
+T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 x1)) w2)) (\lambda (w2:
T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
-w2))))) (eq_ind_r T (THead (Bind b) x0 x1) (\lambda (t: T).(or (pr0 (THead
-(Flat Appl) v1 t) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
-t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 t) w2)) (\lambda
-(w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
-t4)) w2))))) (or_ind (pr0 x1 t4) (ex2 T (\lambda (w2: T).(pr0 x1 w2))
-(\lambda (w2: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4 w2))) (or (pr0
-(THead (Flat Appl) v1 (THead (Bind b) x0 x1)) (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl)
-v1 (THead (Bind b) x0 x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b)
-u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H16: (pr0 x1
-t4)).(or_ind (pr0 x0 u2) (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
-T).(subst0 (s (Flat Appl) i) v3 u2 w2))) (or (pr0 (THead (Flat Appl) v1
+w2)))) (\lambda (H18: (pr0 x0 u2)).(or_introl (pr0 (THead (Flat Appl) v1
(THead (Bind b) x0 x1)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind b)
x0 x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H17: (pr0 x0 u2)).(or_introl
-(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 x1)) (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat
-Appl) v1 (THead (Bind b) x0 x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead
-(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))) (pr0_upsilon b H0
-v1 v2 H1 x0 u2 H17 x1 t4 H16))) (\lambda (H17: (ex2 T (\lambda (w2: T).(pr0
-x0 w2)) (\lambda (w2: T).(subst0 (s (Flat Appl) i) v3 u2 w2)))).(ex2_ind T
-(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 (s (Flat Appl) i) v3
-u2 w2)) (or (pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 x1)) (THead (Bind
-b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0
-(THead (Flat Appl) v1 (THead (Bind b) x0 x1)) w2)) (\lambda (w2: T).(subst0 i
-v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
-(\lambda (x2: T).(\lambda (H18: (pr0 x0 x2)).(\lambda (H19: (subst0 (s (Flat
-Appl) i) v3 u2 x2)).(or_intror (pr0 (THead (Flat Appl) v1 (THead (Bind b) x0
-x1)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
-(\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 x1)) w2))
-(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1
-(THead (Bind b) x0 x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2
-(THead (Flat Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) x2 (THead
-(Flat Appl) (lift (S O) O v2) t4)) (pr0_upsilon b H0 v1 v2 H1 x0 x2 H18 x1 t4
-H16) (subst0_fst v3 x2 u2 i H19 (THead (Flat Appl) (lift (S O) O v2) t4)
-(Bind b))))))) H17)) (H4 v0 x0 (s (Flat Appl) i) H14 v3 H8))) (\lambda (H16:
-(ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda (w2: T).(subst0 (s (Bind b) (s
-(Flat Appl) i)) v3 t4 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x1 w2))
-(\lambda (w2: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4 w2)) (or (pr0
-(THead (Flat Appl) v1 (THead (Bind b) x0 x1)) (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl)
-v1 (THead (Bind b) x0 x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b)
-u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (x2: T).(\lambda
-(H17: (pr0 x1 x2)).(\lambda (H18: (subst0 (s (Bind b) (s (Flat Appl) i)) v3
-t4 x2)).(or_ind (pr0 x0 u2) (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda
-(w2: T).(subst0 (s (Flat Appl) i) v3 u2 w2))) (or (pr0 (THead (Flat Appl) v1
-(THead (Bind b) x0 x1)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
-v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind b)
-x0 x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H19: (pr0 x0 u2)).(or_intror
-(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 x1)) (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat
-Appl) v1 (THead (Bind b) x0 x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead
-(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))) (ex_intro2 T
-(\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 x1)) w2))
-(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
-x2)) (pr0_upsilon b H0 v1 v2 H1 x0 u2 H19 x1 x2 H17) (subst0_snd (Bind b) v3
-(THead (Flat Appl) (lift (S O) O v2) x2) (THead (Flat Appl) (lift (S O) O v2)
-t4) i (subst0_snd (Flat Appl) v3 x2 t4 (s (Bind b) i) H18 (lift (S O) O v2))
-u2)))) (\lambda (H19: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
+Appl) (lift (S O) O v2) t4)) w2))) (pr0_upsilon b H0 v1 v2 H1 x0 u2 H18 x1 t4
+H17))) (\lambda (H18: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
T).(subst0 (s (Flat Appl) i) v3 u2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0
w2)) (\lambda (w2: T).(subst0 (s (Flat Appl) i) v3 u2 w2)) (or (pr0 (THead
(Flat Appl) v1 (THead (Bind b) x0 x1)) (THead (Bind b) u2 (THead (Flat Appl)
(lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1
(THead (Bind b) x0 x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2
-(THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (x3: T).(\lambda
-(H20: (pr0 x0 x3)).(\lambda (H21: (subst0 (s (Flat Appl) i) v3 u2
-x3)).(or_intror (pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 x1)) (THead
+(THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (x2: T).(\lambda
+(H19: (pr0 x0 x2)).(\lambda (H20: (subst0 (s (Flat Appl) i) v3 u2
+x2)).(or_intror (pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 x1)) (THead
(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 x1)) w2)) (\lambda (w2:
T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind
b) x0 x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) x3 (THead (Flat Appl) (lift
-(S O) O v2) x2)) (pr0_upsilon b H0 v1 v2 H1 x0 x3 H20 x1 x2 H17) (subst0_both
-v3 u2 x3 i H21 (Bind b) (THead (Flat Appl) (lift (S O) O v2) t4) (THead (Flat
-Appl) (lift (S O) O v2) x2) (subst0_snd (Flat Appl) v3 x2 t4 (s (Bind b) i)
-H18 (lift (S O) O v2)))))))) H19)) (H4 v0 x0 (s (Flat Appl) i) H14 v3 H8)))))
-H16)) (H6 v0 x1 (s (Bind b) (s (Flat Appl) i)) H15 v3 H8)) x H13) w1
-H10)))))) H12)) (subst0_gen_head (Bind b) v0 u1 t3 x (s (Flat Appl) i)
-H11))))) H9)) (\lambda (H9: (ex3_2 T T (\lambda (u3: T).(\lambda (t5: T).(eq
-T w1 (THead (Flat Appl) u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i
-v0 v1 u3))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s (Flat Appl) i) v0
-(THead (Bind b) u1 t3) t5))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda (t5:
-T).(eq T w1 (THead (Flat Appl) u3 t5)))) (\lambda (u3: T).(\lambda (_:
-T).(subst0 i v0 v1 u3))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s (Flat
-Appl) i) v0 (THead (Bind b) u1 t3) t5))) (or (pr0 w1 (THead (Bind b) u2
-(THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 w1
-w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
-(lift (S O) O v2) t4)) w2)))) (\lambda (x0: T).(\lambda (x1: T).(\lambda
-(H10: (eq T w1 (THead (Flat Appl) x0 x1))).(\lambda (H11: (subst0 i v0 v1
-x0)).(\lambda (H12: (subst0 (s (Flat Appl) i) v0 (THead (Bind b) u1 t3)
-x1)).(or3_ind (ex2 T (\lambda (u3: T).(eq T x1 (THead (Bind b) u3 t3)))
-(\lambda (u3: T).(subst0 (s (Flat Appl) i) v0 u1 u3))) (ex2 T (\lambda (t5:
-T).(eq T x1 (THead (Bind b) u1 t5))) (\lambda (t5: T).(subst0 (s (Bind b) (s
-(Flat Appl) i)) v0 t3 t5))) (ex3_2 T T (\lambda (u3: T).(\lambda (t5: T).(eq
-T x1 (THead (Bind b) u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 (s
-(Flat Appl) i) v0 u1 u3))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s (Bind
-b) (s (Flat Appl) i)) v0 t3 t5)))) (or (pr0 w1 (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 w1 w2))
+Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) x2 (THead (Flat Appl) (lift
+(S O) O v2) t4)) (pr0_upsilon b H0 v1 v2 H1 x0 x2 H19 x1 t4 H17) (subst0_fst
+v3 x2 u2 i H20 (THead (Flat Appl) (lift (S O) O v2) t4) (Bind b))))))) H18))
+(H4 v0 x0 (s (Flat Appl) i) H14 v3 H8))) (\lambda (H17: (ex2 T (\lambda (w2:
+T).(pr0 x1 w2)) (\lambda (w2: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4
+w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x1 w2)) (\lambda (w2: T).(subst0 (s
+(Bind b) (s (Flat Appl) i)) v3 t4 w2)) (or (pr0 (THead (Flat Appl) v1 (THead
+(Bind b) x0 x1)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
+t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0
+x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
+(lift (S O) O v2) t4)) w2)))) (\lambda (x2: T).(\lambda (H18: (pr0 x1
+x2)).(\lambda (H19: (subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4 x2)).(or_ind
+(pr0 x0 u2) (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 (s
+(Flat Appl) i) v3 u2 w2))) (or (pr0 (THead (Flat Appl) v1 (THead (Bind b) x0
+x1)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
+(\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 x1)) w2))
(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2)))) (\lambda (H13: (ex2 T (\lambda (u3: T).(eq T x1 (THead
-(Bind b) u3 t3))) (\lambda (u3: T).(subst0 (s (Flat Appl) i) v0 u1
-u3)))).(ex2_ind T (\lambda (u3: T).(eq T x1 (THead (Bind b) u3 t3))) (\lambda
-(u3: T).(subst0 (s (Flat Appl) i) v0 u1 u3)) (or (pr0 w1 (THead (Bind b) u2
-(THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 w1
-w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
-(lift (S O) O v2) t4)) w2)))) (\lambda (x: T).(\lambda (H14: (eq T x1 (THead
-(Bind b) x t3))).(\lambda (H15: (subst0 (s (Flat Appl) i) v0 u1 x)).(eq_ind_r
-T (THead (Flat Appl) x0 x1) (\lambda (t: T).(or (pr0 t (THead (Bind b) u2
+O) O v2) t4)) w2)))) (\lambda (H20: (pr0 x0 u2)).(or_intror (pr0 (THead (Flat
+Appl) v1 (THead (Bind b) x0 x1)) (THead (Bind b) u2 (THead (Flat Appl) (lift
+(S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead
+(Bind b) x0 x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead
+(Flat Appl) (lift (S O) O v2) t4)) w2))) (ex_intro2 T (\lambda (w2: T).(pr0
+(THead (Flat Appl) v1 (THead (Bind b) x0 x1)) w2)) (\lambda (w2: T).(subst0 i
+v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)) (THead
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) x2)) (pr0_upsilon b H0 v1 v2
+H1 x0 u2 H20 x1 x2 H18) (subst0_snd (Bind b) v3 (THead (Flat Appl) (lift (S
+O) O v2) x2) (THead (Flat Appl) (lift (S O) O v2) t4) i (subst0_snd (Flat
+Appl) v3 x2 t4 (s (Bind b) i) H19 (lift (S O) O v2)) u2)))) (\lambda (H20:
+(ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 (s (Flat Appl)
+i) v3 u2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
+T).(subst0 (s (Flat Appl) i) v3 u2 w2)) (or (pr0 (THead (Flat Appl) v1 (THead
+(Bind b) x0 x1)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
+t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0
+x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
+(lift (S O) O v2) t4)) w2)))) (\lambda (x3: T).(\lambda (H21: (pr0 x0
+x3)).(\lambda (H22: (subst0 (s (Flat Appl) i) v3 u2 x3)).(or_intror (pr0
+(THead (Flat Appl) v1 (THead (Bind b) x0 x1)) (THead (Bind b) u2 (THead (Flat
+Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl)
+v1 (THead (Bind b) x0 x1)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b)
+u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))) (ex_intro2 T (\lambda (w2:
+T).(pr0 (THead (Flat Appl) v1 (THead (Bind b) x0 x1)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
+w2)) (THead (Bind b) x3 (THead (Flat Appl) (lift (S O) O v2) x2))
+(pr0_upsilon b H0 v1 v2 H1 x0 x3 H21 x1 x2 H18) (subst0_both v3 u2 x3 i H22
+(Bind b) (THead (Flat Appl) (lift (S O) O v2) t4) (THead (Flat Appl) (lift (S
+O) O v2) x2) (subst0_snd (Flat Appl) v3 x2 t4 (s (Bind b) i) H19 (lift (S O)
+O v2)))))))) H20)) (H4 v0 x0 (s (Flat Appl) i) H14 v3 H8))))) H17)) (H6 v0 x1
+(s (Bind b) (s (Flat Appl) i)) H15 v3 H8)) w1 H16))))))) H12))
+(subst0_gen_head (Bind b) v0 u1 t3 x (s (Flat Appl) i) H11))))) H9)) (\lambda
+(H9: (ex3_2 T T (\lambda (u3: T).(\lambda (t5: T).(eq T w1 (THead (Flat Appl)
+u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i v0 v1 u3))) (\lambda (_:
+T).(\lambda (t5: T).(subst0 (s (Flat Appl) i) v0 (THead (Bind b) u1 t3)
+t5))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda (t5: T).(eq T w1 (THead
+(Flat Appl) u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i v0 v1 u3)))
+(\lambda (_: T).(\lambda (t5: T).(subst0 (s (Flat Appl) i) v0 (THead (Bind b)
+u1 t3) t5))) (or (pr0 w1 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
+v2) t4))) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v3
+(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda
+(x0: T).(\lambda (x1: T).(\lambda (H10: (eq T w1 (THead (Flat Appl) x0
+x1))).(\lambda (H11: (subst0 i v0 v1 x0)).(\lambda (H12: (subst0 (s (Flat
+Appl) i) v0 (THead (Bind b) u1 t3) x1)).(or3_ind (ex2 T (\lambda (u3: T).(eq
+T x1 (THead (Bind b) u3 t3))) (\lambda (u3: T).(subst0 (s (Flat Appl) i) v0
+u1 u3))) (ex2 T (\lambda (t5: T).(eq T x1 (THead (Bind b) u1 t5))) (\lambda
+(t5: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v0 t3 t5))) (ex3_2 T T
+(\lambda (u3: T).(\lambda (t5: T).(eq T x1 (THead (Bind b) u3 t5)))) (\lambda
+(u3: T).(\lambda (_: T).(subst0 (s (Flat Appl) i) v0 u1 u3))) (\lambda (_:
+T).(\lambda (t5: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v0 t3 t5)))) (or
+(pr0 w1 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
+(\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b)
+u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H13: (ex2 T
+(\lambda (u3: T).(eq T x1 (THead (Bind b) u3 t3))) (\lambda (u3: T).(subst0
+(s (Flat Appl) i) v0 u1 u3)))).(ex2_ind T (\lambda (u3: T).(eq T x1 (THead
+(Bind b) u3 t3))) (\lambda (u3: T).(subst0 (s (Flat Appl) i) v0 u1 u3)) (or
+(pr0 w1 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
+(\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b)
+u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (x: T).(\lambda
+(H14: (eq T x1 (THead (Bind b) x t3))).(\lambda (H15: (subst0 (s (Flat Appl)
+i) v0 u1 x)).(let H16 \def (eq_ind T x1 (\lambda (t: T).(eq T w1 (THead (Flat
+Appl) x0 t))) H10 (THead (Bind b) x t3) H14) in (eq_ind_r T (THead (Flat
+Appl) x0 (THead (Bind b) x t3)) (\lambda (t: T).(or (pr0 t (THead (Bind b) u2
(THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 t
w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
-(lift (S O) O v2) t4)) w2))))) (eq_ind_r T (THead (Bind b) x t3) (\lambda (t:
-T).(or (pr0 (THead (Flat Appl) x0 t) (THead (Bind b) u2 (THead (Flat Appl)
-(lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 t)
-w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
(lift (S O) O v2) t4)) w2))))) (or_ind (pr0 x u2) (ex2 T (\lambda (w2:
T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Flat Appl) i) v3 u2 w2))) (or
(pr0 (THead (Flat Appl) x0 (THead (Bind b) x t3)) (THead (Bind b) u2 (THead
(Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat
Appl) x0 (THead (Bind b) x t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead
-(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H16:
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H17:
(pr0 x u2)).(or_ind (pr0 x0 v2) (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda
(w2: T).(subst0 i v3 v2 w2))) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b)
x t3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
(\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x t3)) w2))
(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2)))) (\lambda (H17: (pr0 x0 v2)).(or_introl (pr0 (THead (Flat
+O) O v2) t4)) w2)))) (\lambda (H18: (pr0 x0 v2)).(or_introl (pr0 (THead (Flat
Appl) x0 (THead (Bind b) x t3)) (THead (Bind b) u2 (THead (Flat Appl) (lift
(S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
(Bind b) x t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O v2) t4)) w2))) (pr0_upsilon b H0 x0 v2 H17 x u2 H16
-t3 t4 H5))) (\lambda (H17: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
+(Flat Appl) (lift (S O) O v2) t4)) w2))) (pr0_upsilon b H0 x0 v2 H18 x u2 H17
+t3 t4 H5))) (\lambda (H18: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
T).(subst0 i v3 v2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda
(w2: T).(subst0 i v3 v2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) x
t3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
(\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x t3)) w2))
(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2)))) (\lambda (x2: T).(\lambda (H18: (pr0 x0 x2)).(\lambda
-(H19: (subst0 i v3 v2 x2)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind
+O) O v2) t4)) w2)))) (\lambda (x2: T).(\lambda (H19: (pr0 x0 x2)).(\lambda
+(H20: (subst0 i v3 v2 x2)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind
b) x t3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2
T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x t3)) w2))
(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
O) O v2) t4)) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0
(THead (Bind b) x t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2
(THead (Flat Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O x2) t4)) (pr0_upsilon b H0 x0 x2 H18 x u2 H16 t3 t4
+(Flat Appl) (lift (S O) O x2) t4)) (pr0_upsilon b H0 x0 x2 H19 x u2 H17 t3 t4
H5) (subst0_snd (Bind b) v3 (THead (Flat Appl) (lift (S O) O x2) t4) (THead
(Flat Appl) (lift (S O) O v2) t4) i (subst0_fst v3 (lift (S O) O x2) (lift (S
-O) O v2) (s (Bind b) i) (subst0_lift_ge_s v2 x2 v3 i H19 O (le_O_n i) b) t4
-(Flat Appl)) u2)))))) H17)) (H2 v0 x0 i H11 v3 H8))) (\lambda (H16: (ex2 T
+O) O v2) (s (Bind b) i) (subst0_lift_ge_s v2 x2 v3 i H20 O (le_O_n i) b) t4
+(Flat Appl)) u2)))))) H18)) (H2 v0 x0 i H11 v3 H8))) (\lambda (H17: (ex2 T
(\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Flat Appl) i) v3 u2
w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s
(Flat Appl) i) v3 u2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) x
t3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
(\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x t3)) w2))
(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2)))) (\lambda (x2: T).(\lambda (H17: (pr0 x x2)).(\lambda
-(H18: (subst0 (s (Flat Appl) i) v3 u2 x2)).(or_ind (pr0 x0 v2) (ex2 T
+O) O v2) t4)) w2)))) (\lambda (x2: T).(\lambda (H18: (pr0 x x2)).(\lambda
+(H19: (subst0 (s (Flat Appl) i) v3 u2 x2)).(or_ind (pr0 x0 v2) (ex2 T
(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2))) (or (pr0
(THead (Flat Appl) x0 (THead (Bind b) x t3)) (THead (Bind b) u2 (THead (Flat
Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl)
x0 (THead (Bind b) x t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b)
-u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H19: (pr0 x0
+u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H20: (pr0 x0
v2)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind b) x t3)) (THead
(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x t3)) w2)) (\lambda (w2:
w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind
b) x t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) x2 (THead (Flat Appl) (lift
-(S O) O v2) t4)) (pr0_upsilon b H0 x0 v2 H19 x x2 H17 t3 t4 H5) (subst0_fst
-v3 x2 u2 i H18 (THead (Flat Appl) (lift (S O) O v2) t4) (Bind b))))) (\lambda
-(H19: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2
+(S O) O v2) t4)) (pr0_upsilon b H0 x0 v2 H20 x x2 H18 t3 t4 H5) (subst0_fst
+v3 x2 u2 i H19 (THead (Flat Appl) (lift (S O) O v2) t4) (Bind b))))) (\lambda
+(H20: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2
w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3
v2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) x t3)) (THead (Bind b)
u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0
(THead (Flat Appl) x0 (THead (Bind b) x t3)) w2)) (\lambda (w2: T).(subst0 i
v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
-(\lambda (x3: T).(\lambda (H20: (pr0 x0 x3)).(\lambda (H21: (subst0 i v3 v2
+(\lambda (x3: T).(\lambda (H21: (pr0 x0 x3)).(\lambda (H22: (subst0 i v3 v2
x3)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind b) x t3)) (THead
(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x t3)) w2)) (\lambda (w2:
w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind
b) x t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) x2 (THead (Flat Appl) (lift
-(S O) O x3) t4)) (pr0_upsilon b H0 x0 x3 H20 x x2 H17 t3 t4 H5) (subst0_both
-v3 u2 x2 i H18 (Bind b) (THead (Flat Appl) (lift (S O) O v2) t4) (THead (Flat
+(S O) O x3) t4)) (pr0_upsilon b H0 x0 x3 H21 x x2 H18 t3 t4 H5) (subst0_both
+v3 u2 x2 i H19 (Bind b) (THead (Flat Appl) (lift (S O) O v2) t4) (THead (Flat
Appl) (lift (S O) O x3) t4) (subst0_fst v3 (lift (S O) O x3) (lift (S O) O
-v2) (s (Bind b) i) (subst0_lift_ge_s v2 x3 v3 i H21 O (le_O_n i) b) t4 (Flat
-Appl)))))))) H19)) (H2 v0 x0 i H11 v3 H8))))) H16)) (H4 v0 x (s (Flat Appl)
-i) H15 v3 H8)) x1 H14) w1 H10)))) H13)) (\lambda (H13: (ex2 T (\lambda (t5:
-T).(eq T x1 (THead (Bind b) u1 t5))) (\lambda (t5: T).(subst0 (s (Bind b) (s
-(Flat Appl) i)) v0 t3 t5)))).(ex2_ind T (\lambda (t5: T).(eq T x1 (THead
-(Bind b) u1 t5))) (\lambda (t5: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v0
-t3 t5)) (or (pr0 w1 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
-t4))) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v3
-(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda
-(x: T).(\lambda (H14: (eq T x1 (THead (Bind b) u1 x))).(\lambda (H15: (subst0
-(s (Bind b) (s (Flat Appl) i)) v0 t3 x)).(eq_ind_r T (THead (Flat Appl) x0
-x1) (\lambda (t: T).(or (pr0 t (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i
-v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))))
-(eq_ind_r T (THead (Bind b) u1 x) (\lambda (t: T).(or (pr0 (THead (Flat Appl)
-x0 t) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
-(\lambda (w2: T).(pr0 (THead (Flat Appl) x0 t) w2)) (\lambda (w2: T).(subst0
-i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))))
-(or_ind (pr0 x t4) (ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2:
-T).(subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4 w2))) (or (pr0 (THead (Flat
+v2) (s (Bind b) i) (subst0_lift_ge_s v2 x3 v3 i H22 O (le_O_n i) b) t4 (Flat
+Appl)))))))) H20)) (H2 v0 x0 i H11 v3 H8))))) H17)) (H4 v0 x (s (Flat Appl)
+i) H15 v3 H8)) w1 H16))))) H13)) (\lambda (H13: (ex2 T (\lambda (t5: T).(eq T
+x1 (THead (Bind b) u1 t5))) (\lambda (t5: T).(subst0 (s (Bind b) (s (Flat
+Appl) i)) v0 t3 t5)))).(ex2_ind T (\lambda (t5: T).(eq T x1 (THead (Bind b)
+u1 t5))) (\lambda (t5: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v0 t3 t5))
+(or (pr0 w1 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)))
+(ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v3 (THead
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (x:
+T).(\lambda (H14: (eq T x1 (THead (Bind b) u1 x))).(\lambda (H15: (subst0 (s
+(Bind b) (s (Flat Appl) i)) v0 t3 x)).(let H16 \def (eq_ind T x1 (\lambda (t:
+T).(eq T w1 (THead (Flat Appl) x0 t))) H10 (THead (Bind b) u1 x) H14) in
+(eq_ind_r T (THead (Flat Appl) x0 (THead (Bind b) u1 x)) (\lambda (t: T).(or
+(pr0 t (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
+(\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2
+(THead (Flat Appl) (lift (S O) O v2) t4)) w2))))) (or_ind (pr0 x t4) (ex2 T
+(\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Bind b) (s (Flat
+Appl) i)) v3 t4 w2))) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x))
+(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda
+(w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
+w2)))) (\lambda (H17: (pr0 x t4)).(or_ind (pr0 x0 v2) (ex2 T (\lambda (w2:
+T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2))) (or (pr0 (THead (Flat
Appl) x0 (THead (Bind b) u1 x)) (THead (Bind b) u2 (THead (Flat Appl) (lift
(S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
(Bind b) u1 x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H16: (pr0 x t4)).(or_ind
+(Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H18: (pr0 x0
+v2)).(or_introl (pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) (THead
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
+T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
+w2))) (pr0_upsilon b H0 x0 v2 H18 u1 u2 H3 x t4 H17))) (\lambda (H18: (ex2 T
+(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2
+w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3
+v2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) (THead (Bind b)
+u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0
+(THead (Flat Appl) x0 (THead (Bind b) u1 x)) w2)) (\lambda (w2: T).(subst0 i
+v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
+(\lambda (x2: T).(\lambda (H19: (pr0 x0 x2)).(\lambda (H20: (subst0 i v3 v2
+x2)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) (THead
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
+T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
+w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind
+b) u1 x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
+Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) u2 (THead (Flat Appl) (lift
+(S O) O x2) t4)) (pr0_upsilon b H0 x0 x2 H19 u1 u2 H3 x t4 H17) (subst0_snd
+(Bind b) v3 (THead (Flat Appl) (lift (S O) O x2) t4) (THead (Flat Appl) (lift
+(S O) O v2) t4) i (subst0_fst v3 (lift (S O) O x2) (lift (S O) O v2) (s (Bind
+b) i) (subst0_lift_ge_s v2 x2 v3 i H20 O (le_O_n i) b) t4 (Flat Appl))
+u2)))))) H18)) (H2 v0 x0 i H11 v3 H8))) (\lambda (H17: (ex2 T (\lambda (w2:
+T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4
+w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s
+(Bind b) (s (Flat Appl) i)) v3 t4 w2)) (or (pr0 (THead (Flat Appl) x0 (THead
+(Bind b) u1 x)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)))
+(ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x))
+w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
+(lift (S O) O v2) t4)) w2)))) (\lambda (x2: T).(\lambda (H18: (pr0 x
+x2)).(\lambda (H19: (subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4 x2)).(or_ind
(pr0 x0 v2) (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i
v3 v2 w2))) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) (THead
(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) w2)) (\lambda (w2:
T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
-w2)))) (\lambda (H17: (pr0 x0 v2)).(or_introl (pr0 (THead (Flat Appl) x0
+w2)))) (\lambda (H20: (pr0 x0 v2)).(or_intror (pr0 (THead (Flat Appl) x0
(THead (Bind b) u1 x)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b)
u1 x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4)) w2))) (pr0_upsilon b H0 x0 v2 H17 u1 u2 H3 x t4
-H16))) (\lambda (H17: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
-T).(subst0 i v3 v2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda
-(w2: T).(subst0 i v3 v2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b)
-u1 x)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
-(\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) w2))
-(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2)))) (\lambda (x2: T).(\lambda (H18: (pr0 x0 x2)).(\lambda
-(H19: (subst0 i v3 v2 x2)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind
-b) u1 x)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2
-T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) w2))
-(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0
-(THead (Bind b) u1 x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2
-(THead (Flat Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O x2) t4)) (pr0_upsilon b H0 x0 x2 H18 u1 u2 H3 x t4
-H16) (subst0_snd (Bind b) v3 (THead (Flat Appl) (lift (S O) O x2) t4) (THead
-(Flat Appl) (lift (S O) O v2) t4) i (subst0_fst v3 (lift (S O) O x2) (lift (S
-O) O v2) (s (Bind b) i) (subst0_lift_ge_s v2 x2 v3 i H19 O (le_O_n i) b) t4
-(Flat Appl)) u2)))))) H17)) (H2 v0 x0 i H11 v3 H8))) (\lambda (H16: (ex2 T
-(\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Bind b) (s (Flat
-Appl) i)) v3 t4 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2:
-T).(subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4 w2)) (or (pr0 (THead (Flat
-Appl) x0 (THead (Bind b) u1 x)) (THead (Bind b) u2 (THead (Flat Appl) (lift
-(S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
-(Bind b) u1 x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (x2: T).(\lambda (H17:
-(pr0 x x2)).(\lambda (H18: (subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4
-x2)).(or_ind (pr0 x0 v2) (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
-T).(subst0 i v3 v2 w2))) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) u1
-x)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
-(\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) w2))
-(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2)))) (\lambda (H19: (pr0 x0 v2)).(or_intror (pr0 (THead (Flat
-Appl) x0 (THead (Bind b) u1 x)) (THead (Bind b) u2 (THead (Flat Appl) (lift
-(S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
-(Bind b) u1 x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O v2) t4)) w2))) (ex_intro2 T (\lambda (w2: T).(pr0
-(THead (Flat Appl) x0 (THead (Bind b) u1 x)) w2)) (\lambda (w2: T).(subst0 i
-v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)) (THead
+Appl) (lift (S O) O v2) t4)) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead
+(Flat Appl) x0 (THead (Bind b) u1 x)) w2)) (\lambda (w2: T).(subst0 i v3
+(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)) (THead
(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) x2)) (pr0_upsilon b H0 x0 v2
-H19 u1 u2 H3 x x2 H17) (subst0_snd (Bind b) v3 (THead (Flat Appl) (lift (S O)
+H20 u1 u2 H3 x x2 H18) (subst0_snd (Bind b) v3 (THead (Flat Appl) (lift (S O)
O v2) x2) (THead (Flat Appl) (lift (S O) O v2) t4) i (subst0_snd (Flat Appl)
-v3 x2 t4 (s (Bind b) i) H18 (lift (S O) O v2)) u2)))) (\lambda (H19: (ex2 T
+v3 x2 t4 (s (Bind b) i) H19 (lift (S O) O v2)) u2)))) (\lambda (H20: (ex2 T
(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2
w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3
v2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) (THead (Bind b)
u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0
(THead (Flat Appl) x0 (THead (Bind b) u1 x)) w2)) (\lambda (w2: T).(subst0 i
v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
-(\lambda (x3: T).(\lambda (H20: (pr0 x0 x3)).(\lambda (H21: (subst0 i v3 v2
+(\lambda (x3: T).(\lambda (H21: (pr0 x0 x3)).(\lambda (H22: (subst0 i v3 v2
x3)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) (THead
(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) u1 x)) w2)) (\lambda (w2:
w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind
b) u1 x)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) u2 (THead (Flat Appl) (lift
-(S O) O x3) x2)) (pr0_upsilon b H0 x0 x3 H20 u1 u2 H3 x x2 H17) (subst0_snd
+(S O) O x3) x2)) (pr0_upsilon b H0 x0 x3 H21 u1 u2 H3 x x2 H18) (subst0_snd
(Bind b) v3 (THead (Flat Appl) (lift (S O) O x3) x2) (THead (Flat Appl) (lift
(S O) O v2) t4) i (subst0_both v3 (lift (S O) O v2) (lift (S O) O x3) (s
-(Bind b) i) (subst0_lift_ge_s v2 x3 v3 i H21 O (le_O_n i) b) (Flat Appl) t4
-x2 H18) u2)))))) H19)) (H2 v0 x0 i H11 v3 H8))))) H16)) (H6 v0 x (s (Bind b)
-(s (Flat Appl) i)) H15 v3 H8)) x1 H14) w1 H10)))) H13)) (\lambda (H13: (ex3_2
-T T (\lambda (u3: T).(\lambda (t5: T).(eq T x1 (THead (Bind b) u3 t5))))
-(\lambda (u3: T).(\lambda (_: T).(subst0 (s (Flat Appl) i) v0 u1 u3)))
-(\lambda (_: T).(\lambda (t5: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v0 t3
+(Bind b) i) (subst0_lift_ge_s v2 x3 v3 i H22 O (le_O_n i) b) (Flat Appl) t4
+x2 H19) u2)))))) H20)) (H2 v0 x0 i H11 v3 H8))))) H17)) (H6 v0 x (s (Bind b)
+(s (Flat Appl) i)) H15 v3 H8)) w1 H16))))) H13)) (\lambda (H13: (ex3_2 T T
+(\lambda (u3: T).(\lambda (t5: T).(eq T x1 (THead (Bind b) u3 t5)))) (\lambda
+(u3: T).(\lambda (_: T).(subst0 (s (Flat Appl) i) v0 u1 u3))) (\lambda (_:
+T).(\lambda (t5: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v0 t3
t5))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda (t5: T).(eq T x1 (THead
(Bind b) u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 (s (Flat Appl) i)
v0 u1 u3))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s (Bind b) (s (Flat
T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
w2)))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H14: (eq T x1 (THead (Bind
b) x2 x3))).(\lambda (H15: (subst0 (s (Flat Appl) i) v0 u1 x2)).(\lambda
-(H16: (subst0 (s (Bind b) (s (Flat Appl) i)) v0 t3 x3)).(eq_ind_r T (THead
-(Flat Appl) x0 x1) (\lambda (t: T).(or (pr0 t (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda
-(w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
-t4)) w2))))) (eq_ind_r T (THead (Bind b) x2 x3) (\lambda (t: T).(or (pr0
-(THead (Flat Appl) x0 t) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
-v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 t) w2)) (\lambda
-(w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
-t4)) w2))))) (or_ind (pr0 x3 t4) (ex2 T (\lambda (w2: T).(pr0 x3 w2))
-(\lambda (w2: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4 w2))) (or (pr0
-(THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl)
-x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b)
-u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H17: (pr0 x3
-t4)).(or_ind (pr0 x2 u2) (ex2 T (\lambda (w2: T).(pr0 x2 w2)) (\lambda (w2:
-T).(subst0 (s (Flat Appl) i) v3 u2 w2))) (or (pr0 (THead (Flat Appl) x0
-(THead (Bind b) x2 x3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
-v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b)
-x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H18: (pr0 x2 u2)).(or_ind (pr0
-x0 v2) (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2
-w2))) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead (Bind b)
-u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0
-(THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i
-v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
-(\lambda (H19: (pr0 x0 v2)).(or_introl (pr0 (THead (Flat Appl) x0 (THead
+(H16: (subst0 (s (Bind b) (s (Flat Appl) i)) v0 t3 x3)).(let H17 \def (eq_ind
+T x1 (\lambda (t: T).(eq T w1 (THead (Flat Appl) x0 t))) H10 (THead (Bind b)
+x2 x3) H14) in (eq_ind_r T (THead (Flat Appl) x0 (THead (Bind b) x2 x3))
+(\lambda (t: T).(or (pr0 t (THead (Bind b) u2 (THead (Flat Appl) (lift (S O)
+O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v3
+(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))) (or_ind
+(pr0 x3 t4) (ex2 T (\lambda (w2: T).(pr0 x3 w2)) (\lambda (w2: T).(subst0 (s
+(Bind b) (s (Flat Appl) i)) v3 t4 w2))) (or (pr0 (THead (Flat Appl) x0 (THead
(Bind b) x2 x3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2
x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
-(lift (S O) O v2) t4)) w2))) (pr0_upsilon b H0 x0 v2 H19 x2 u2 H18 x3 t4
-H17))) (\lambda (H19: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
-T).(subst0 i v3 v2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda
-(w2: T).(subst0 i v3 v2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b)
-x2 x3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
-(\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2))
-(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2)))) (\lambda (x: T).(\lambda (H20: (pr0 x0 x)).(\lambda
-(H21: (subst0 i v3 v2 x)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind
-b) x2 x3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2
-T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2))
-(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0
-(THead (Bind b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2
-(THead (Flat Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O x) t4)) (pr0_upsilon b H0 x0 x H20 x2 u2 H18 x3 t4
-H17) (subst0_snd (Bind b) v3 (THead (Flat Appl) (lift (S O) O x) t4) (THead
-(Flat Appl) (lift (S O) O v2) t4) i (subst0_fst v3 (lift (S O) O x) (lift (S
-O) O v2) (s (Bind b) i) (subst0_lift_ge_s v2 x v3 i H21 O (le_O_n i) b) t4
-(Flat Appl)) u2)))))) H19)) (H2 v0 x0 i H11 v3 H8))) (\lambda (H18: (ex2 T
-(\lambda (w2: T).(pr0 x2 w2)) (\lambda (w2: T).(subst0 (s (Flat Appl) i) v3
-u2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x2 w2)) (\lambda (w2: T).(subst0
-(s (Flat Appl) i) v3 u2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b)
-x2 x3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
+(lift (S O) O v2) t4)) w2)))) (\lambda (H18: (pr0 x3 t4)).(or_ind (pr0 x2 u2)
+(ex2 T (\lambda (w2: T).(pr0 x2 w2)) (\lambda (w2: T).(subst0 (s (Flat Appl)
+i) v3 u2 w2))) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
+T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
+w2)))) (\lambda (H19: (pr0 x2 u2)).(or_ind (pr0 x0 v2) (ex2 T (\lambda (w2:
+T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2))) (or (pr0 (THead (Flat
+Appl) x0 (THead (Bind b) x2 x3)) (THead (Bind b) u2 (THead (Flat Appl) (lift
+(S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead
+(Bind b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead
+(Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H20: (pr0 x0
+v2)).(or_introl (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
+T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
+w2))) (pr0_upsilon b H0 x0 v2 H20 x2 u2 H19 x3 t4 H18))) (\lambda (H20: (ex2
+T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2
+w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3
+v2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead (Bind
+b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0
+(THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i
+v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
+(\lambda (x: T).(\lambda (H21: (pr0 x0 x)).(\lambda (H22: (subst0 i v3 v2
+x)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead
+(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
+T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2:
+T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
+w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind
+b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
+Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) u2 (THead (Flat Appl) (lift
+(S O) O x) t4)) (pr0_upsilon b H0 x0 x H21 x2 u2 H19 x3 t4 H18) (subst0_snd
+(Bind b) v3 (THead (Flat Appl) (lift (S O) O x) t4) (THead (Flat Appl) (lift
+(S O) O v2) t4) i (subst0_fst v3 (lift (S O) O x) (lift (S O) O v2) (s (Bind
+b) i) (subst0_lift_ge_s v2 x v3 i H22 O (le_O_n i) b) t4 (Flat Appl))
+u2)))))) H20)) (H2 v0 x0 i H11 v3 H8))) (\lambda (H19: (ex2 T (\lambda (w2:
+T).(pr0 x2 w2)) (\lambda (w2: T).(subst0 (s (Flat Appl) i) v3 u2
+w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x2 w2)) (\lambda (w2: T).(subst0 (s
+(Flat Appl) i) v3 u2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2
+x3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
(\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2))
(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2)))) (\lambda (x: T).(\lambda (H19: (pr0 x2 x)).(\lambda
-(H20: (subst0 (s (Flat Appl) i) v3 u2 x)).(or_ind (pr0 x0 v2) (ex2 T (\lambda
+O) O v2) t4)) w2)))) (\lambda (x: T).(\lambda (H20: (pr0 x2 x)).(\lambda
+(H21: (subst0 (s (Flat Appl) i) v3 u2 x)).(or_ind (pr0 x0 v2) (ex2 T (\lambda
(w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2))) (or (pr0 (THead
(Flat Appl) x0 (THead (Bind b) x2 x3)) (THead (Bind b) u2 (THead (Flat Appl)
(lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0
(THead (Bind b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2
-(THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H21: (pr0 x0
+(THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H22: (pr0 x0
v2)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead
(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2:
w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind
b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) x (THead (Flat Appl) (lift
-(S O) O v2) t4)) (pr0_upsilon b H0 x0 v2 H21 x2 x H19 x3 t4 H17) (subst0_fst
-v3 x u2 i H20 (THead (Flat Appl) (lift (S O) O v2) t4) (Bind b))))) (\lambda
-(H21: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2
+(S O) O v2) t4)) (pr0_upsilon b H0 x0 v2 H22 x2 x H20 x3 t4 H18) (subst0_fst
+v3 x u2 i H21 (THead (Flat Appl) (lift (S O) O v2) t4) (Bind b))))) (\lambda
+(H22: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2
w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3
v2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead (Bind
b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0
(THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i
v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
-(\lambda (x4: T).(\lambda (H22: (pr0 x0 x4)).(\lambda (H23: (subst0 i v3 v2
+(\lambda (x4: T).(\lambda (H23: (pr0 x0 x4)).(\lambda (H24: (subst0 i v3 v2
x4)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead
(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2:
w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind
b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) x (THead (Flat Appl) (lift
-(S O) O x4) t4)) (pr0_upsilon b H0 x0 x4 H22 x2 x H19 x3 t4 H17) (subst0_both
-v3 u2 x i H20 (Bind b) (THead (Flat Appl) (lift (S O) O v2) t4) (THead (Flat
+(S O) O x4) t4)) (pr0_upsilon b H0 x0 x4 H23 x2 x H20 x3 t4 H18) (subst0_both
+v3 u2 x i H21 (Bind b) (THead (Flat Appl) (lift (S O) O v2) t4) (THead (Flat
Appl) (lift (S O) O x4) t4) (subst0_fst v3 (lift (S O) O x4) (lift (S O) O
-v2) (s (Bind b) i) (subst0_lift_ge_s v2 x4 v3 i H23 O (le_O_n i) b) t4 (Flat
-Appl)))))))) H21)) (H2 v0 x0 i H11 v3 H8))))) H18)) (H4 v0 x2 (s (Flat Appl)
-i) H15 v3 H8))) (\lambda (H17: (ex2 T (\lambda (w2: T).(pr0 x3 w2)) (\lambda
+v2) (s (Bind b) i) (subst0_lift_ge_s v2 x4 v3 i H24 O (le_O_n i) b) t4 (Flat
+Appl)))))))) H22)) (H2 v0 x0 i H11 v3 H8))))) H19)) (H4 v0 x2 (s (Flat Appl)
+i) H15 v3 H8))) (\lambda (H18: (ex2 T (\lambda (w2: T).(pr0 x3 w2)) (\lambda
(w2: T).(subst0 (s (Bind b) (s (Flat Appl) i)) v3 t4 w2)))).(ex2_ind T
(\lambda (w2: T).(pr0 x3 w2)) (\lambda (w2: T).(subst0 (s (Bind b) (s (Flat
Appl) i)) v3 t4 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3))
(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda
(w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2:
T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))
-w2)))) (\lambda (x: T).(\lambda (H18: (pr0 x3 x)).(\lambda (H19: (subst0 (s
+w2)))) (\lambda (x: T).(\lambda (H19: (pr0 x3 x)).(\lambda (H20: (subst0 (s
(Bind b) (s (Flat Appl) i)) v3 t4 x)).(or_ind (pr0 x2 u2) (ex2 T (\lambda
(w2: T).(pr0 x2 w2)) (\lambda (w2: T).(subst0 (s (Flat Appl) i) v3 u2 w2)))
(or (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead (Bind b) u2
(THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0
(THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i
v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
-(\lambda (H20: (pr0 x2 u2)).(or_ind (pr0 x0 v2) (ex2 T (\lambda (w2: T).(pr0
+(\lambda (H21: (pr0 x2 u2)).(or_ind (pr0 x0 v2) (ex2 T (\lambda (w2: T).(pr0
x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2))) (or (pr0 (THead (Flat Appl) x0
(THead (Bind b) x2 x3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O
v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b)
x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
-Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H21: (pr0 x0 v2)).(or_intror
+Appl) (lift (S O) O v2) t4)) w2)))) (\lambda (H22: (pr0 x0 v2)).(or_intror
(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead (Bind b) u2 (THead
(Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat
Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead
(\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2))
(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
O) O v2) t4)) w2)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
-x)) (pr0_upsilon b H0 x0 v2 H21 x2 u2 H20 x3 x H18) (subst0_snd (Bind b) v3
+x)) (pr0_upsilon b H0 x0 v2 H22 x2 u2 H21 x3 x H19) (subst0_snd (Bind b) v3
(THead (Flat Appl) (lift (S O) O v2) x) (THead (Flat Appl) (lift (S O) O v2)
-t4) i (subst0_snd (Flat Appl) v3 x t4 (s (Bind b) i) H19 (lift (S O) O v2))
-u2)))) (\lambda (H21: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
+t4) i (subst0_snd (Flat Appl) v3 x t4 (s (Bind b) i) H20 (lift (S O) O v2))
+u2)))) (\lambda (H22: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2:
T).(subst0 i v3 v2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda
(w2: T).(subst0 i v3 v2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b)
x2 x3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T
(\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2))
(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
-O) O v2) t4)) w2)))) (\lambda (x4: T).(\lambda (H22: (pr0 x0 x4)).(\lambda
-(H23: (subst0 i v3 v2 x4)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind
+O) O v2) t4)) w2)))) (\lambda (x4: T).(\lambda (H23: (pr0 x0 x4)).(\lambda
+(H24: (subst0 i v3 v2 x4)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind
b) x2 x3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2
T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2))
(\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S
O) O v2) t4)) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0
(THead (Bind b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2
(THead (Flat Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) u2 (THead
-(Flat Appl) (lift (S O) O x4) x)) (pr0_upsilon b H0 x0 x4 H22 x2 u2 H20 x3 x
-H18) (subst0_snd (Bind b) v3 (THead (Flat Appl) (lift (S O) O x4) x) (THead
+(Flat Appl) (lift (S O) O x4) x)) (pr0_upsilon b H0 x0 x4 H23 x2 u2 H21 x3 x
+H19) (subst0_snd (Bind b) v3 (THead (Flat Appl) (lift (S O) O x4) x) (THead
(Flat Appl) (lift (S O) O v2) t4) i (subst0_both v3 (lift (S O) O v2) (lift
-(S O) O x4) (s (Bind b) i) (subst0_lift_ge_s v2 x4 v3 i H23 O (le_O_n i) b)
-(Flat Appl) t4 x H19) u2)))))) H21)) (H2 v0 x0 i H11 v3 H8))) (\lambda (H20:
+(S O) O x4) (s (Bind b) i) (subst0_lift_ge_s v2 x4 v3 i H24 O (le_O_n i) b)
+(Flat Appl) t4 x H20) u2)))))) H22)) (H2 v0 x0 i H11 v3 H8))) (\lambda (H21:
(ex2 T (\lambda (w2: T).(pr0 x2 w2)) (\lambda (w2: T).(subst0 (s (Flat Appl)
i) v3 u2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x2 w2)) (\lambda (w2:
T).(subst0 (s (Flat Appl) i) v3 u2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead
(Bind b) x2 x3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2
x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
-(lift (S O) O v2) t4)) w2)))) (\lambda (x4: T).(\lambda (H21: (pr0 x2
-x4)).(\lambda (H22: (subst0 (s (Flat Appl) i) v3 u2 x4)).(or_ind (pr0 x0 v2)
+(lift (S O) O v2) t4)) w2)))) (\lambda (x4: T).(\lambda (H22: (pr0 x2
+x4)).(\lambda (H23: (subst0 (s (Flat Appl) i) v3 u2 x4)).(or_ind (pr0 x0 v2)
(ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2 w2)))
(or (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead (Bind b) u2
(THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0
(THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i
v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
-(\lambda (H23: (pr0 x0 v2)).(or_intror (pr0 (THead (Flat Appl) x0 (THead
+(\lambda (H24: (pr0 x0 v2)).(or_intror (pr0 (THead (Flat Appl) x0 (THead
(Bind b) x2 x3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2)
t4))) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2
x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat Appl)
(lift (S O) O v2) t4)) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat
Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead
(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) x4
-(THead (Flat Appl) (lift (S O) O v2) x)) (pr0_upsilon b H0 x0 v2 H23 x2 x4
-H21 x3 x H18) (subst0_both v3 u2 x4 i H22 (Bind b) (THead (Flat Appl) (lift
+(THead (Flat Appl) (lift (S O) O v2) x)) (pr0_upsilon b H0 x0 v2 H24 x2 x4
+H22 x3 x H19) (subst0_both v3 u2 x4 i H23 (Bind b) (THead (Flat Appl) (lift
(S O) O v2) t4) (THead (Flat Appl) (lift (S O) O v2) x) (subst0_snd (Flat
-Appl) v3 x t4 (s (Bind b) i) H19 (lift (S O) O v2)))))) (\lambda (H23: (ex2 T
+Appl) v3 x t4 (s (Bind b) i) H20 (lift (S O) O v2)))))) (\lambda (H24: (ex2 T
(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3 v2
w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v3
v2 w2)) (or (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead (Bind
b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0
(THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i
v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2))))
-(\lambda (x5: T).(\lambda (H24: (pr0 x0 x5)).(\lambda (H25: (subst0 i v3 v2
+(\lambda (x5: T).(\lambda (H25: (pr0 x0 x5)).(\lambda (H26: (subst0 i v3 v2
x5)).(or_intror (pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) (THead
(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2:
T).(pr0 (THead (Flat Appl) x0 (THead (Bind b) x2 x3)) w2)) (\lambda (w2:
w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Appl) x0 (THead (Bind
b) x2 x3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead (Bind b) u2 (THead (Flat
Appl) (lift (S O) O v2) t4)) w2)) (THead (Bind b) x4 (THead (Flat Appl) (lift
-(S O) O x5) x)) (pr0_upsilon b H0 x0 x5 H24 x2 x4 H21 x3 x H18) (subst0_both
-v3 u2 x4 i H22 (Bind b) (THead (Flat Appl) (lift (S O) O v2) t4) (THead (Flat
+(S O) O x5) x)) (pr0_upsilon b H0 x0 x5 H25 x2 x4 H22 x3 x H19) (subst0_both
+v3 u2 x4 i H23 (Bind b) (THead (Flat Appl) (lift (S O) O v2) t4) (THead (Flat
Appl) (lift (S O) O x5) x) (subst0_both v3 (lift (S O) O v2) (lift (S O) O
-x5) (s (Bind b) i) (subst0_lift_ge_s v2 x5 v3 i H25 O (le_O_n i) b) (Flat
-Appl) t4 x H19))))))) H23)) (H2 v0 x0 i H11 v3 H8))))) H20)) (H4 v0 x2 (s
-(Flat Appl) i) H15 v3 H8))))) H17)) (H6 v0 x3 (s (Bind b) (s (Flat Appl) i))
-H16 v3 H8)) x1 H14) w1 H10)))))) H13)) (subst0_gen_head (Bind b) v0 u1 t3 x1
-(s (Flat Appl) i) H12))))))) H9)) (subst0_gen_head (Flat Appl) v0 v1 (THead
+x5) (s (Bind b) i) (subst0_lift_ge_s v2 x5 v3 i H26 O (le_O_n i) b) (Flat
+Appl) t4 x H20))))))) H24)) (H2 v0 x0 i H11 v3 H8))))) H21)) (H4 v0 x2 (s
+(Flat Appl) i) H15 v3 H8))))) H18)) (H6 v0 x3 (s (Bind b) (s (Flat Appl) i))
+H16 v3 H8)) w1 H17))))))) H13)) (subst0_gen_head (Bind b) v0 u1 t3 x1 (s
+(Flat Appl) i) H12))))))) H9)) (subst0_gen_head (Flat Appl) v0 v1 (THead
(Bind b) u1 t3) w1 i H7)))))))))))))))))))))) (\lambda (u1: T).(\lambda (u2:
T).(\lambda (H0: (pr0 u1 u2)).(\lambda (H1: ((\forall (v1: T).(\forall (w1:
T).(\forall (i: nat).((subst0 i v1 u1 w1) \to (\forall (v2: T).((pr0 v1 v2)
(\lambda (t5: T).(subst0 (minus (s (Bind b) i) (S O)) v1 t3 t5)) (or (pr0 w1
t4) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 t4
w2)))) (\lambda (x0: T).(\lambda (H8: (eq T x (lift (S O) O x0))).(\lambda
-(H9: (subst0 (minus (s (Bind b) i) (S O)) v1 t3 x0)).(eq_ind_r T (THead (Bind
-b) u x) (\lambda (t: T).(or (pr0 t t4) (ex2 T (\lambda (w2: T).(pr0 t w2))
-(\lambda (w2: T).(subst0 i v2 t4 w2))))) (eq_ind_r T (lift (S O) O x0)
-(\lambda (t: T).(or (pr0 (THead (Bind b) u t) t4) (ex2 T (\lambda (w2:
-T).(pr0 (THead (Bind b) u t) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))))
-(let H10 \def (eq_ind_r nat (minus i O) (\lambda (n: nat).(subst0 n v1 t3
-x0)) H9 i (minus_n_O i)) in (or_ind (pr0 x0 t4) (ex2 T (\lambda (w2: T).(pr0
-x0 w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (or (pr0 (THead (Bind b) u
-(lift (S O) O x0)) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind b) u (lift
-(S O) O x0)) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (H11: (pr0
-x0 t4)).(or_introl (pr0 (THead (Bind b) u (lift (S O) O x0)) t4) (ex2 T
-(\lambda (w2: T).(pr0 (THead (Bind b) u (lift (S O) O x0)) w2)) (\lambda (w2:
-T).(subst0 i v2 t4 w2))) (pr0_zeta b H0 x0 t4 H11 u))) (\lambda (H11: (ex2 T
-(\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v2 t4
+(H9: (subst0 (minus (s (Bind b) i) (S O)) v1 t3 x0)).(let H10 \def (eq_ind T
+x (\lambda (t: T).(eq T w1 (THead (Bind b) u t))) H6 (lift (S O) O x0) H8) in
+(eq_ind_r T (THead (Bind b) u (lift (S O) O x0)) (\lambda (t: T).(or (pr0 t
+t4) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v2 t4
+w2))))) (let H11 \def (eq_ind_r nat (minus i O) (\lambda (n: nat).(subst0 n
+v1 t3 x0)) H9 i (minus_n_O i)) in (or_ind (pr0 x0 t4) (ex2 T (\lambda (w2:
+T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (or (pr0 (THead (Bind
+b) u (lift (S O) O x0)) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind b) u
+(lift (S O) O x0)) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda
+(H12: (pr0 x0 t4)).(or_introl (pr0 (THead (Bind b) u (lift (S O) O x0)) t4)
+(ex2 T (\lambda (w2: T).(pr0 (THead (Bind b) u (lift (S O) O x0)) w2))
+(\lambda (w2: T).(subst0 i v2 t4 w2))) (pr0_zeta b H0 x0 t4 H12 u))) (\lambda
+(H12: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v2 t4
w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v2
t4 w2)) (or (pr0 (THead (Bind b) u (lift (S O) O x0)) t4) (ex2 T (\lambda
(w2: T).(pr0 (THead (Bind b) u (lift (S O) O x0)) w2)) (\lambda (w2:
-T).(subst0 i v2 t4 w2)))) (\lambda (x1: T).(\lambda (H12: (pr0 x0
-x1)).(\lambda (H13: (subst0 i v2 t4 x1)).(or_intror (pr0 (THead (Bind b) u
+T).(subst0 i v2 t4 w2)))) (\lambda (x1: T).(\lambda (H13: (pr0 x0
+x1)).(\lambda (H14: (subst0 i v2 t4 x1)).(or_intror (pr0 (THead (Bind b) u
(lift (S O) O x0)) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind b) u (lift
(S O) O x0)) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (ex_intro2 T
(\lambda (w2: T).(pr0 (THead (Bind b) u (lift (S O) O x0)) w2)) (\lambda (w2:
-T).(subst0 i v2 t4 w2)) x1 (pr0_zeta b H0 x0 x1 H12 u) H13))))) H11)) (H2 v1
-x0 i H10 v2 H4))) x H8) w1 H6)))) (subst0_gen_lift_ge v1 t3 x (s (Bind b) i)
-(S O) O H7 (le_n_S O i (le_O_n i))))))) H5)) (\lambda (H5: (ex3_2 T T
-(\lambda (u2: T).(\lambda (t5: T).(eq T w1 (THead (Bind b) u2 t5)))) (\lambda
-(u2: T).(\lambda (_: T).(subst0 i v1 u u2))) (\lambda (_: T).(\lambda (t5:
+T).(subst0 i v2 t4 w2)) x1 (pr0_zeta b H0 x0 x1 H13 u) H14))))) H12)) (H2 v1
+x0 i H11 v2 H4))) w1 H10))))) (subst0_gen_lift_ge v1 t3 x (s (Bind b) i) (S
+O) O H7 (le_n_S O i (le_O_n i))))))) H5)) (\lambda (H5: (ex3_2 T T (\lambda
+(u2: T).(\lambda (t5: T).(eq T w1 (THead (Bind b) u2 t5)))) (\lambda (u2:
+T).(\lambda (_: T).(subst0 i v1 u u2))) (\lambda (_: T).(\lambda (t5:
T).(subst0 (s (Bind b) i) v1 (lift (S O) O t3) t5))))).(ex3_2_ind T T
(\lambda (u2: T).(\lambda (t5: T).(eq T w1 (THead (Bind b) u2 t5)))) (\lambda
(u2: T).(\lambda (_: T).(subst0 i v1 u u2))) (\lambda (_: T).(\lambda (t5:
t5))) (\lambda (t5: T).(subst0 (minus (s (Bind b) i) (S O)) v1 t3 t5)) (or
(pr0 w1 t4) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i
v2 t4 w2)))) (\lambda (x: T).(\lambda (H9: (eq T x1 (lift (S O) O
-x))).(\lambda (H10: (subst0 (minus (s (Bind b) i) (S O)) v1 t3 x)).(eq_ind_r
-T (THead (Bind b) x0 x1) (\lambda (t: T).(or (pr0 t t4) (ex2 T (\lambda (w2:
-T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))))) (eq_ind_r T (lift (S
-O) O x) (\lambda (t: T).(or (pr0 (THead (Bind b) x0 t) t4) (ex2 T (\lambda
-(w2: T).(pr0 (THead (Bind b) x0 t) w2)) (\lambda (w2: T).(subst0 i v2 t4
-w2))))) (let H11 \def (eq_ind_r nat (minus i O) (\lambda (n: nat).(subst0 n
-v1 t3 x)) H10 i (minus_n_O i)) in (or_ind (pr0 x t4) (ex2 T (\lambda (w2:
-T).(pr0 x w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (or (pr0 (THead (Bind
-b) x0 (lift (S O) O x)) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind b) x0
-(lift (S O) O x)) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (H12:
-(pr0 x t4)).(or_introl (pr0 (THead (Bind b) x0 (lift (S O) O x)) t4) (ex2 T
+x))).(\lambda (H10: (subst0 (minus (s (Bind b) i) (S O)) v1 t3 x)).(let H11
+\def (eq_ind T x1 (\lambda (t: T).(eq T w1 (THead (Bind b) x0 t))) H6 (lift
+(S O) O x) H9) in (eq_ind_r T (THead (Bind b) x0 (lift (S O) O x)) (\lambda
+(t: T).(or (pr0 t t4) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2:
+T).(subst0 i v2 t4 w2))))) (let H12 \def (eq_ind_r nat (minus i O) (\lambda
+(n: nat).(subst0 n v1 t3 x)) H10 i (minus_n_O i)) in (or_ind (pr0 x t4) (ex2
+T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (or
+(pr0 (THead (Bind b) x0 (lift (S O) O x)) t4) (ex2 T (\lambda (w2: T).(pr0
+(THead (Bind b) x0 (lift (S O) O x)) w2)) (\lambda (w2: T).(subst0 i v2 t4
+w2)))) (\lambda (H13: (pr0 x t4)).(or_introl (pr0 (THead (Bind b) x0 (lift (S
+O) O x)) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind b) x0 (lift (S O) O
+x)) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (pr0_zeta b H0 x t4 H13 x0)))
+(\lambda (H13: (ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 i
+v2 t4 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0
+i v2 t4 w2)) (or (pr0 (THead (Bind b) x0 (lift (S O) O x)) t4) (ex2 T
(\lambda (w2: T).(pr0 (THead (Bind b) x0 (lift (S O) O x)) w2)) (\lambda (w2:
-T).(subst0 i v2 t4 w2))) (pr0_zeta b H0 x t4 H12 x0))) (\lambda (H12: (ex2 T
-(\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))).(ex2_ind
-T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)) (or (pr0
-(THead (Bind b) x0 (lift (S O) O x)) t4) (ex2 T (\lambda (w2: T).(pr0 (THead
-(Bind b) x0 (lift (S O) O x)) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))))
-(\lambda (x2: T).(\lambda (H13: (pr0 x x2)).(\lambda (H14: (subst0 i v2 t4
-x2)).(or_intror (pr0 (THead (Bind b) x0 (lift (S O) O x)) t4) (ex2 T (\lambda
+T).(subst0 i v2 t4 w2)))) (\lambda (x2: T).(\lambda (H14: (pr0 x
+x2)).(\lambda (H15: (subst0 i v2 t4 x2)).(or_intror (pr0 (THead (Bind b) x0
+(lift (S O) O x)) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind b) x0 (lift
+(S O) O x)) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (ex_intro2 T (\lambda
(w2: T).(pr0 (THead (Bind b) x0 (lift (S O) O x)) w2)) (\lambda (w2:
-T).(subst0 i v2 t4 w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Bind b)
-x0 (lift (S O) O x)) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)) x2 (pr0_zeta
-b H0 x x2 H13 x0) H14))))) H12)) (H2 v1 x i H11 v2 H4))) x1 H9) w1 H6))))
-(subst0_gen_lift_ge v1 t3 x1 (s (Bind b) i) (S O) O H8 (le_n_S O i (le_O_n
-i))))))))) H5)) (subst0_gen_head (Bind b) v1 u (lift (S O) O t3) w1 i
-H3))))))))))))))) (\lambda (t3: T).(\lambda (t4: T).(\lambda (H0: (pr0 t3
-t4)).(\lambda (H1: ((\forall (v1: T).(\forall (w1: T).(\forall (i:
-nat).((subst0 i v1 t3 w1) \to (\forall (v2: T).((pr0 v1 v2) \to (or (pr0 w1
-t4) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 t4
-w2)))))))))))).(\lambda (u: T).(\lambda (v1: T).(\lambda (w1: T).(\lambda (i:
-nat).(\lambda (H2: (subst0 i v1 (THead (Flat Cast) u t3) w1)).(\lambda (v2:
-T).(\lambda (H3: (pr0 v1 v2)).(or3_ind (ex2 T (\lambda (u2: T).(eq T w1
-(THead (Flat Cast) u2 t3))) (\lambda (u2: T).(subst0 i v1 u u2))) (ex2 T
-(\lambda (t5: T).(eq T w1 (THead (Flat Cast) u t5))) (\lambda (t5: T).(subst0
-(s (Flat Cast) i) v1 t3 t5))) (ex3_2 T T (\lambda (u2: T).(\lambda (t5:
-T).(eq T w1 (THead (Flat Cast) u2 t5)))) (\lambda (u2: T).(\lambda (_:
-T).(subst0 i v1 u u2))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s (Flat
-Cast) i) v1 t3 t5)))) (or (pr0 w1 t4) (ex2 T (\lambda (w2: T).(pr0 w1 w2))
-(\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (H4: (ex2 T (\lambda (u2:
-T).(eq T w1 (THead (Flat Cast) u2 t3))) (\lambda (u2: T).(subst0 i v1 u
-u2)))).(ex2_ind T (\lambda (u2: T).(eq T w1 (THead (Flat Cast) u2 t3)))
-(\lambda (u2: T).(subst0 i v1 u u2)) (or (pr0 w1 t4) (ex2 T (\lambda (w2:
-T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (x:
-T).(\lambda (H5: (eq T w1 (THead (Flat Cast) x t3))).(\lambda (_: (subst0 i
-v1 u x)).(eq_ind_r T (THead (Flat Cast) x t3) (\lambda (t: T).(or (pr0 t t4)
-(ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))))
-(or_introl (pr0 (THead (Flat Cast) x t3) t4) (ex2 T (\lambda (w2: T).(pr0
-(THead (Flat Cast) x t3) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))
-(pr0_epsilon t3 t4 H0 x)) w1 H5)))) H4)) (\lambda (H4: (ex2 T (\lambda (t5:
-T).(eq T w1 (THead (Flat Cast) u t5))) (\lambda (t5: T).(subst0 (s (Flat
-Cast) i) v1 t3 t5)))).(ex2_ind T (\lambda (t5: T).(eq T w1 (THead (Flat Cast)
-u t5))) (\lambda (t5: T).(subst0 (s (Flat Cast) i) v1 t3 t5)) (or (pr0 w1 t4)
-(ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))))
-(\lambda (x: T).(\lambda (H5: (eq T w1 (THead (Flat Cast) u x))).(\lambda
-(H6: (subst0 (s (Flat Cast) i) v1 t3 x)).(eq_ind_r T (THead (Flat Cast) u x)
-(\lambda (t: T).(or (pr0 t t4) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda
-(w2: T).(subst0 i v2 t4 w2))))) (or_ind (pr0 x t4) (ex2 T (\lambda (w2:
-T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Flat Cast) i) v2 t4 w2))) (or
-(pr0 (THead (Flat Cast) u x) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat
-Cast) u x) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (H7: (pr0 x
-t4)).(or_introl (pr0 (THead (Flat Cast) u x) t4) (ex2 T (\lambda (w2: T).(pr0
-(THead (Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))
-(pr0_epsilon x t4 H7 u))) (\lambda (H7: (ex2 T (\lambda (w2: T).(pr0 x w2))
-(\lambda (w2: T).(subst0 (s (Flat Cast) i) v2 t4 w2)))).(ex2_ind T (\lambda
-(w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Flat Cast) i) v2 t4 w2)) (or
-(pr0 (THead (Flat Cast) u x) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat
-Cast) u x) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (x0:
+T).(subst0 i v2 t4 w2)) x2 (pr0_zeta b H0 x x2 H14 x0) H15))))) H13)) (H2 v1
+x i H12 v2 H4))) w1 H11))))) (subst0_gen_lift_ge v1 t3 x1 (s (Bind b) i) (S
+O) O H8 (le_n_S O i (le_O_n i))))))))) H5)) (subst0_gen_head (Bind b) v1 u
+(lift (S O) O t3) w1 i H3))))))))))))))) (\lambda (t3: T).(\lambda (t4:
+T).(\lambda (H0: (pr0 t3 t4)).(\lambda (H1: ((\forall (v1: T).(\forall (w1:
+T).(\forall (i: nat).((subst0 i v1 t3 w1) \to (\forall (v2: T).((pr0 v1 v2)
+\to (or (pr0 w1 t4) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2:
+T).(subst0 i v2 t4 w2)))))))))))).(\lambda (u: T).(\lambda (v1: T).(\lambda
+(w1: T).(\lambda (i: nat).(\lambda (H2: (subst0 i v1 (THead (Flat Cast) u t3)
+w1)).(\lambda (v2: T).(\lambda (H3: (pr0 v1 v2)).(or3_ind (ex2 T (\lambda
+(u2: T).(eq T w1 (THead (Flat Cast) u2 t3))) (\lambda (u2: T).(subst0 i v1 u
+u2))) (ex2 T (\lambda (t5: T).(eq T w1 (THead (Flat Cast) u t5))) (\lambda
+(t5: T).(subst0 (s (Flat Cast) i) v1 t3 t5))) (ex3_2 T T (\lambda (u2:
+T).(\lambda (t5: T).(eq T w1 (THead (Flat Cast) u2 t5)))) (\lambda (u2:
+T).(\lambda (_: T).(subst0 i v1 u u2))) (\lambda (_: T).(\lambda (t5:
+T).(subst0 (s (Flat Cast) i) v1 t3 t5)))) (or (pr0 w1 t4) (ex2 T (\lambda
+(w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (H4:
+(ex2 T (\lambda (u2: T).(eq T w1 (THead (Flat Cast) u2 t3))) (\lambda (u2:
+T).(subst0 i v1 u u2)))).(ex2_ind T (\lambda (u2: T).(eq T w1 (THead (Flat
+Cast) u2 t3))) (\lambda (u2: T).(subst0 i v1 u u2)) (or (pr0 w1 t4) (ex2 T
+(\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))))
+(\lambda (x: T).(\lambda (H5: (eq T w1 (THead (Flat Cast) x t3))).(\lambda
+(_: (subst0 i v1 u x)).(eq_ind_r T (THead (Flat Cast) x t3) (\lambda (t:
+T).(or (pr0 t t4) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2:
+T).(subst0 i v2 t4 w2))))) (or_introl (pr0 (THead (Flat Cast) x t3) t4) (ex2
+T (\lambda (w2: T).(pr0 (THead (Flat Cast) x t3) w2)) (\lambda (w2:
+T).(subst0 i v2 t4 w2))) (pr0_tau t3 t4 H0 x)) w1 H5)))) H4)) (\lambda (H4:
+(ex2 T (\lambda (t5: T).(eq T w1 (THead (Flat Cast) u t5))) (\lambda (t5:
+T).(subst0 (s (Flat Cast) i) v1 t3 t5)))).(ex2_ind T (\lambda (t5: T).(eq T
+w1 (THead (Flat Cast) u t5))) (\lambda (t5: T).(subst0 (s (Flat Cast) i) v1
+t3 t5)) (or (pr0 w1 t4) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2:
+T).(subst0 i v2 t4 w2)))) (\lambda (x: T).(\lambda (H5: (eq T w1 (THead (Flat
+Cast) u x))).(\lambda (H6: (subst0 (s (Flat Cast) i) v1 t3 x)).(eq_ind_r T
+(THead (Flat Cast) u x) (\lambda (t: T).(or (pr0 t t4) (ex2 T (\lambda (w2:
+T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))))) (or_ind (pr0 x t4)
+(ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Flat Cast)
+i) v2 t4 w2))) (or (pr0 (THead (Flat Cast) u x) t4) (ex2 T (\lambda (w2:
+T).(pr0 (THead (Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))))
+(\lambda (H7: (pr0 x t4)).(or_introl (pr0 (THead (Flat Cast) u x) t4) (ex2 T
+(\lambda (w2: T).(pr0 (THead (Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 i
+v2 t4 w2))) (pr0_tau x t4 H7 u))) (\lambda (H7: (ex2 T (\lambda (w2: T).(pr0
+x w2)) (\lambda (w2: T).(subst0 (s (Flat Cast) i) v2 t4 w2)))).(ex2_ind T
+(\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Flat Cast) i) v2 t4
+w2)) (or (pr0 (THead (Flat Cast) u x) t4) (ex2 T (\lambda (w2: T).(pr0 (THead
+(Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (x0:
T).(\lambda (H8: (pr0 x x0)).(\lambda (H9: (subst0 (s (Flat Cast) i) v2 t4
x0)).(or_intror (pr0 (THead (Flat Cast) u x) t4) (ex2 T (\lambda (w2: T).(pr0
(THead (Flat Cast) u x) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))
(ex_intro2 T (\lambda (w2: T).(pr0 (THead (Flat Cast) u x) w2)) (\lambda (w2:
-T).(subst0 i v2 t4 w2)) x0 (pr0_epsilon x x0 H8 u) H9))))) H7)) (H1 v1 x (s
-(Flat Cast) i) H6 v2 H3)) w1 H5)))) H4)) (\lambda (H4: (ex3_2 T T (\lambda
-(u2: T).(\lambda (t5: T).(eq T w1 (THead (Flat Cast) u2 t5)))) (\lambda (u2:
+T).(subst0 i v2 t4 w2)) x0 (pr0_tau x x0 H8 u) H9))))) H7)) (H1 v1 x (s (Flat
+Cast) i) H6 v2 H3)) w1 H5)))) H4)) (\lambda (H4: (ex3_2 T T (\lambda (u2:
+T).(\lambda (t5: T).(eq T w1 (THead (Flat Cast) u2 t5)))) (\lambda (u2:
T).(\lambda (_: T).(subst0 i v1 u u2))) (\lambda (_: T).(\lambda (t5:
T).(subst0 (s (Flat Cast) i) v1 t3 t5))))).(ex3_2_ind T T (\lambda (u2:
T).(\lambda (t5: T).(eq T w1 (THead (Flat Cast) u2 t5)))) (\lambda (u2:
x1) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Cast) x0 x1) w2)) (\lambda
(w2: T).(subst0 i v2 t4 w2)))) (\lambda (H8: (pr0 x1 t4)).(or_introl (pr0
(THead (Flat Cast) x0 x1) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Cast)
-x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (pr0_epsilon x1 t4 H8
-x0))) (\lambda (H8: (ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda (w2:
-T).(subst0 (s (Flat Cast) i) v2 t4 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x1
-w2)) (\lambda (w2: T).(subst0 (s (Flat Cast) i) v2 t4 w2)) (or (pr0 (THead
+x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (pr0_tau x1 t4 H8 x0)))
+(\lambda (H8: (ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda (w2: T).(subst0
+(s (Flat Cast) i) v2 t4 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x1 w2))
+(\lambda (w2: T).(subst0 (s (Flat Cast) i) v2 t4 w2)) (or (pr0 (THead (Flat
+Cast) x0 x1) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Cast) x0 x1) w2))
+(\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (x: T).(\lambda (H9: (pr0 x1
+x)).(\lambda (H10: (subst0 (s (Flat Cast) i) v2 t4 x)).(or_intror (pr0 (THead
(Flat Cast) x0 x1) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat Cast) x0 x1)
-w2)) (\lambda (w2: T).(subst0 i v2 t4 w2)))) (\lambda (x: T).(\lambda (H9:
-(pr0 x1 x)).(\lambda (H10: (subst0 (s (Flat Cast) i) v2 t4 x)).(or_intror
-(pr0 (THead (Flat Cast) x0 x1) t4) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat
-Cast) x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (ex_intro2 T
-(\lambda (w2: T).(pr0 (THead (Flat Cast) x0 x1) w2)) (\lambda (w2: T).(subst0
-i v2 t4 w2)) x (pr0_epsilon x1 x H9 x0) H10))))) H8)) (H1 v1 x1 (s (Flat
-Cast) i) H7 v2 H3)) w1 H5)))))) H4)) (subst0_gen_head (Flat Cast) v1 u t3 w1
-i H2))))))))))))) t1 t2 H))).
+w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))) (ex_intro2 T (\lambda (w2:
+T).(pr0 (THead (Flat Cast) x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 t4 w2))
+x (pr0_tau x1 x H9 x0) H10))))) H8)) (H1 v1 x1 (s (Flat Cast) i) H7 v2 H3))
+w1 H5)))))) H4)) (subst0_gen_head (Flat Cast) v1 u t3 w1 i H2))))))))))))) t1
+t2 H))).
projects / helm.git / blobdiff