X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=matita%2Fmatita%2Fcontribs%2Flambdadelta%2Fbasic_1%2Fpr0%2Fprops.ma;h=d1c31fcc74cbd0a845cfcae819158f6b132c1a9e;hb=57ae1762497a5f3ea75740e2908e04adb8642cc2;hp=d7f69d691abb71849d095ce10739f316e6dd9c78;hpb=88a68a9c334646bc17314d5327cd3b790202acd6;p=helm.git diff --git a/matita/matita/contribs/lambdadelta/basic_1/pr0/props.ma b/matita/matita/contribs/lambdadelta/basic_1/pr0/props.ma index d7f69d691..d1c31fcc7 100644 --- a/matita/matita/contribs/lambdadelta/basic_1/pr0/props.ma +++ b/matita/matita/contribs/lambdadelta/basic_1/pr0/props.ma @@ -14,11 +14,11 @@ (* This file was automatically generated: do not edit *********************) -include "Basic-1/pr0/defs.ma". +include "basic_1/pr0/fwd.ma". -include "Basic-1/subst0/subst0.ma". +include "basic_1/subst0/props.ma". -theorem pr0_lift: +lemma pr0_lift: \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (h: nat).(\forall (d: nat).(pr0 (lift h d t1) (lift h d t2)))))) \def @@ -104,1655 +104,431 @@ 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' 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 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 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 -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) -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))). -(* COMMENTS -Initial nodes: 2845 -END *) - -theorem pr0_subst0_back: - \forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst0 -i u2 t1 t2) \to (\forall (u1: T).((pr0 u1 u2) \to (ex2 T (\lambda (t: -T).(subst0 i u1 t1 t)) (\lambda (t: T).(pr0 t t2))))))))) -\def - \lambda (u2: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (i: nat).(\lambda -(H: (subst0 i u2 t1 t2)).(subst0_ind (\lambda (n: nat).(\lambda (t: -T).(\lambda (t0: T).(\lambda (t3: T).(\forall (u1: T).((pr0 u1 t) \to (ex2 T -(\lambda (t4: T).(subst0 n u1 t0 t4)) (\lambda (t4: T).(pr0 t4 t3))))))))) -(\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 (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))))). -(* COMMENTS -Initial nodes: 979 -END *) +(le_O_n d)) h) d (eq_ind nat d (\lambda (n: nat).(eq nat n d)) (le_antisym d +d (le_n d) (le_n 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 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 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 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) 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_fwd: - \forall (u2: T).(\forall (t1: T).(\forall (t2: T).(\forall (i: nat).((subst0 -i u2 t1 t2) \to (\forall (u1: T).((pr0 u2 u1) \to (ex2 T (\lambda (t: -T).(subst0 i u1 t1 t)) (\lambda (t: T).(pr0 t2 t))))))))) +lemma pr0_gen_abbr: + \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Abbr) u1 +t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead +(Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda +(u2: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T (\lambda (y: T).(pr0 t1 y)) +(\lambda (y: T).(subst0 O u2 y t2))))))) (pr0 t1 (lift (S O) O x)))))) \def - \lambda (u2: T).(\lambda (t1: T).(\lambda (t2: T).(\lambda (i: nat).(\lambda -(H: (subst0 i u2 t1 t2)).(subst0_ind (\lambda (n: nat).(\lambda (t: -T).(\lambda (t0: T).(\lambda (t3: T).(\forall (u1: T).((pr0 t u1) \to (ex2 T -(\lambda (t4: T).(subst0 n u1 t0 t4)) (\lambda (t4: T).(pr0 t3 t4))))))))) -(\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 (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 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))))). -(* COMMENTS -Initial nodes: 979 -END *) + \lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (H: (pr0 (THead +(Bind Abbr) u1 t1) x)).(insert_eq T (THead (Bind Abbr) u1 t1) (\lambda (t: +T).(pr0 t x)) (\lambda (_: T).(or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: +T).(eq T x (THead (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 +u1 u2))) (\lambda (u2: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T (\lambda +(y: T).(pr0 t1 y)) (\lambda (y: T).(subst0 O u2 y t2))))))) (pr0 t1 (lift (S +O) O x)))) (\lambda (y: T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t: +T).(\lambda (t0: T).((eq T t (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T +(\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Bind Abbr) u2 t2)))) +(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t2: +T).(or (pr0 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: +T).(subst0 O u2 y0 t2))))))) (pr0 t1 (lift (S O) O t0)))))) (\lambda (t: +T).(\lambda (H1: (eq T t (THead (Bind Abbr) u1 t1))).(let H2 \def (f_equal T +T (\lambda (e: T).e) t (THead (Bind Abbr) u1 t1) H1) in (eq_ind_r T (THead +(Bind Abbr) u1 t1) (\lambda (t0: T).(or (ex3_2 T T (\lambda (u2: T).(\lambda +(t2: T).(eq T t0 (THead (Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: +T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T +(\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0 t2))))))) (pr0 +t1 (lift (S O) O t0)))) (or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t2: +T).(eq T (THead (Bind Abbr) u1 t1) (THead (Bind Abbr) u2 t2)))) (\lambda (u2: +T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t2: T).(or (pr0 +t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0 +t2))))))) (pr0 t1 (lift (S O) O (THead (Bind Abbr) u1 t1))) (ex3_2_intro T T +(\lambda (u2: T).(\lambda (t2: T).(eq T (THead (Bind Abbr) u1 t1) (THead +(Bind Abbr) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda +(u2: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) +(\lambda (y0: T).(subst0 O u2 y0 t2)))))) u1 t1 (refl_equal T (THead (Bind +Abbr) u1 t1)) (pr0_refl u1) (or_introl (pr0 t1 t1) (ex2 T (\lambda (y0: +T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u1 y0 t1))) (pr0_refl t1)))) t +H2)))) (\lambda (u0: T).(\lambda (u2: T).(\lambda (H1: (pr0 u0 u2)).(\lambda +(H2: (((eq T u0 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: +T).(\lambda (t2: T).(eq T u2 (THead (Bind Abbr) u3 t2)))) (\lambda (u3: +T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t2: T).(or (pr0 +t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 +t2))))))) (pr0 t1 (lift (S O) O u2)))))).(\lambda (t0: T).(\lambda (t2: +T).(\lambda (H3: (pr0 t0 t2)).(\lambda (H4: (((eq T t0 (THead (Bind Abbr) u1 +t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead +(Bind Abbr) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda +(u3: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) +(\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O +t2)))))).(\lambda (k: K).(\lambda (H5: (eq T (THead k u0 t0) (THead (Bind +Abbr) u1 t1))).(let H6 \def (f_equal T K (\lambda (e: T).(match e with +[(TSort _) \Rightarrow k | (TLRef _) \Rightarrow k | (THead k0 _ _) +\Rightarrow k0])) (THead k u0 t0) (THead (Bind Abbr) u1 t1) H5) in ((let H7 +\def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow u0 | +(TLRef _) \Rightarrow u0 | (THead _ t _) \Rightarrow t])) (THead k u0 t0) +(THead (Bind Abbr) u1 t1) H5) in ((let H8 \def (f_equal T T (\lambda (e: +T).(match e with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | +(THead _ _ t) \Rightarrow t])) (THead k u0 t0) (THead (Bind Abbr) u1 t1) H5) +in (\lambda (H9: (eq T u0 u1)).(\lambda (H10: (eq K k (Bind Abbr))).(eq_ind_r +K (Bind Abbr) (\lambda (k0: K).(or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: +T).(eq T (THead k0 u2 t2) (THead (Bind Abbr) u3 t3)))) (\lambda (u3: +T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3: T).(or (pr0 +t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 +t3))))))) (pr0 t1 (lift (S O) O (THead k0 u2 t2))))) (let H11 \def (eq_ind T +t0 (\lambda (t: T).((eq T t (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T +(\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u3 t3)))) +(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3: +T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: +T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O t2))))) H4 t1 H8) in (let +H12 \def (eq_ind T t0 (\lambda (t: T).(pr0 t t2)) H3 t1 H8) in (let H13 \def +(eq_ind T u0 (\lambda (t: T).((eq T t (THead (Bind Abbr) u1 t1)) \to (or +(ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T u2 (THead (Bind Abbr) u3 +t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: +T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) +(\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O u2))))) H2 +u1 H9) in (let H14 \def (eq_ind T u0 (\lambda (t: T).(pr0 t u2)) H1 u1 H9) in +(or_introl (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind +Abbr) u2 t2) (THead (Bind Abbr) u3 t3)))) (\lambda (u3: T).(\lambda (_: +T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T +(\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0 +t1 (lift (S O) O (THead (Bind Abbr) u2 t2))) (ex3_2_intro T T (\lambda (u3: +T).(\lambda (t3: T).(eq T (THead (Bind Abbr) u2 t2) (THead (Bind Abbr) u3 +t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: +T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) +(\lambda (y0: T).(subst0 O u3 y0 t3)))))) u2 t2 (refl_equal T (THead (Bind +Abbr) u2 t2)) H14 (or_introl (pr0 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) +(\lambda (y0: T).(subst0 O u2 y0 t2))) H12))))))) k H10)))) H7)) +H6)))))))))))) (\lambda (u: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: +(pr0 v1 v2)).(\lambda (_: (((eq T v1 (THead (Bind Abbr) u1 t1)) \to (or +(ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind Abbr) u2 +t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: +T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) +(\lambda (y0: T).(subst0 O u2 y0 t2))))))) (pr0 t1 (lift (S O) O +v2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda +(_: (((eq T t0 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u2: +T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))) (\lambda (u2: +T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t3: T).(or (pr0 +t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0 +t3))))))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (H5: (eq T (THead (Flat +Appl) v1 (THead (Bind Abst) u t0)) (THead (Bind Abbr) u1 t1))).(let H6 \def +(eq_ind T (THead (Flat Appl) v1 (THead (Bind Abst) u t0)) (\lambda (ee: +T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False +| (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat +_) \Rightarrow True])])) I (THead (Bind Abbr) u1 t1) H5) in (False_ind (or +(ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) v2 t2) +(THead (Bind Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) +(\lambda (u2: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: +T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S +O) O (THead (Bind Abbr) v2 t2)))) H6)))))))))))) (\lambda (b: B).(\lambda (_: +(not (eq B b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 +v2)).(\lambda (_: (((eq T v1 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T +(\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind Abbr) u2 t2)))) +(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t2: +T).(or (pr0 t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: +T).(subst0 O u2 y0 t2))))))) (pr0 t1 (lift (S O) O v2)))))).(\lambda (u0: +T).(\lambda (u2: T).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (((eq T u0 (THead +(Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq +T u2 (THead (Bind Abbr) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 +u3))) (\lambda (u3: T).(\lambda (t2: T).(or (pr0 t1 t2) (ex2 T (\lambda (y0: +T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 t2))))))) (pr0 t1 (lift (S +O) O u2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 +t2)).(\lambda (_: (((eq T t0 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T +(\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u3 t3)))) +(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3: +T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: +T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (H8: (eq +T (THead (Flat Appl) v1 (THead (Bind b) u0 t0)) (THead (Bind Abbr) u1 +t1))).(let H9 \def (eq_ind T (THead (Flat Appl) v1 (THead (Bind b) u0 t0)) +(\lambda (ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) +\Rightarrow False | (THead k _ _) \Rightarrow (match k with [(Bind _) +\Rightarrow False | (Flat _) \Rightarrow True])])) I (THead (Bind Abbr) u1 +t1) H8) in (False_ind (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T +(THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2)) (THead (Bind +Abbr) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: +T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) +(\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O (THead (Bind +b) u2 (THead (Flat Appl) (lift (S O) O v2) t2))))) H9))))))))))))))))) +(\lambda (u0: T).(\lambda (u2: T).(\lambda (H1: (pr0 u0 u2)).(\lambda (H2: +(((eq T u0 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: +T).(\lambda (t2: T).(eq T u2 (THead (Bind Abbr) u3 t2)))) (\lambda (u3: +T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t2: T).(or (pr0 +t1 t2) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 +t2))))))) (pr0 t1 (lift (S O) O u2)))))).(\lambda (t0: T).(\lambda (t2: +T).(\lambda (H3: (pr0 t0 t2)).(\lambda (H4: (((eq T t0 (THead (Bind Abbr) u1 +t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead +(Bind Abbr) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda +(u3: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) +(\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O +t2)))))).(\lambda (w: T).(\lambda (H5: (subst0 O u2 t2 w)).(\lambda (H6: (eq +T (THead (Bind Abbr) u0 t0) (THead (Bind Abbr) u1 t1))).(let H7 \def (f_equal +T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow u0 | (TLRef _) +\Rightarrow u0 | (THead _ t _) \Rightarrow t])) (THead (Bind Abbr) u0 t0) +(THead (Bind Abbr) u1 t1) H6) in ((let H8 \def (f_equal T T (\lambda (e: +T).(match e with [(TSort _) \Rightarrow t0 | (TLRef _) \Rightarrow t0 | +(THead _ _ t) \Rightarrow t])) (THead (Bind Abbr) u0 t0) (THead (Bind Abbr) +u1 t1) H6) in (\lambda (H9: (eq T u0 u1)).(let H10 \def (eq_ind T t0 (\lambda +(t: T).((eq T t (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: +T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u3 t3)))) (\lambda (u3: +T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3: T).(or (pr0 +t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 +t3))))))) (pr0 t1 (lift (S O) O t2))))) H4 t1 H8) in (let H11 \def (eq_ind T +t0 (\lambda (t: T).(pr0 t t2)) H3 t1 H8) in (let H12 \def (eq_ind T u0 +(\lambda (t: T).((eq T t (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T +(\lambda (u3: T).(\lambda (t3: T).(eq T u2 (THead (Bind Abbr) u3 t3)))) +(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3: +T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: +T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S O) O u2))))) H2 u1 H9) in (let +H13 \def (eq_ind T u0 (\lambda (t: T).(pr0 t u2)) H1 u1 H9) in (or_introl +(ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) u2 w) +(THead (Bind Abbr) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) +(\lambda (u3: T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: +T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u3 y0 t3))))))) (pr0 t1 (lift (S +O) O (THead (Bind Abbr) u2 w))) (ex3_2_intro T T (\lambda (u3: T).(\lambda +(t3: T).(eq T (THead (Bind Abbr) u2 w) (THead (Bind Abbr) u3 t3)))) (\lambda +(u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (u3: T).(\lambda (t3: T).(or +(pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O +u3 y0 t3)))))) u2 w (refl_equal T (THead (Bind Abbr) u2 w)) H13 (or_intror +(pr0 t1 w) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O u2 +y0 w))) (ex_intro2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: T).(subst0 O +u2 y0 w)) t2 H11 H5)))))))))) H7))))))))))))) (\lambda (b: B).(\lambda (H1: +(not (eq B b Abst))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H2: (pr0 t0 +t2)).(\lambda (H3: (((eq T t0 (THead (Bind Abbr) u1 t1)) \to (or (ex3_2 T T +(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 t3)))) +(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: T).(\lambda (t3: +T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) (\lambda (y0: +T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (u: +T).(\lambda (H4: (eq T (THead (Bind b) u (lift (S O) O t0)) (THead (Bind +Abbr) u1 t1))).(let H5 \def (f_equal T B (\lambda (e: T).(match e with +[(TSort _) \Rightarrow b | (TLRef _) \Rightarrow b | (THead k _ _) +\Rightarrow (match k with [(Bind b0) \Rightarrow b0 | (Flat _) \Rightarrow +b])])) (THead (Bind b) u (lift (S O) O t0)) (THead (Bind Abbr) u1 t1) H4) in +((let H6 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) +\Rightarrow u | (TLRef _) \Rightarrow u | (THead _ t _) \Rightarrow t])) +(THead (Bind b) u (lift (S O) O t0)) (THead (Bind Abbr) u1 t1) H4) in ((let +H7 \def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow +(lref_map (\lambda (x0: nat).(plus x0 (S O))) O t0) | (TLRef _) \Rightarrow +(lref_map (\lambda (x0: nat).(plus x0 (S O))) O t0) | (THead _ _ t) +\Rightarrow t])) (THead (Bind b) u (lift (S O) O t0)) (THead (Bind Abbr) u1 +t1) H4) in (\lambda (_: (eq T u u1)).(\lambda (H9: (eq B b Abbr)).(let H10 +\def (eq_ind B b (\lambda (b0: B).(not (eq B b0 Abst))) H1 Abbr H9) in (let +H11 \def (eq_ind_r T t1 (\lambda (t: T).((eq T t0 (THead (Bind Abbr) u1 t)) +\to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind +Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: +T).(\lambda (t3: T).(or (pr0 t t3) (ex2 T (\lambda (y0: T).(pr0 t y0)) +(\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t (lift (S O) O t2))))) H3 +(lift (S O) O t0) H7) in (eq_ind T (lift (S O) O t0) (\lambda (t: T).(or +(ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 +t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: +T).(\lambda (t3: T).(or (pr0 t t3) (ex2 T (\lambda (y0: T).(pr0 t y0)) +(\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t (lift (S O) O t2)))) +(or_intror (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind +Abbr) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: +T).(\lambda (t3: T).(or (pr0 (lift (S O) O t0) t3) (ex2 T (\lambda (y0: +T).(pr0 (lift (S O) O t0) y0)) (\lambda (y0: T).(subst0 O u2 y0 t3))))))) +(pr0 (lift (S O) O t0) (lift (S O) O t2)) (pr0_lift t0 t2 H2 (S O) O)) t1 +H7)))))) H6)) H5)))))))))) (\lambda (t0: T).(\lambda (t2: T).(\lambda (_: +(pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind Abbr) u1 t1)) \to (or +(ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) u2 +t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: +T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) +(\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S O) O +t2)))))).(\lambda (u: T).(\lambda (H3: (eq T (THead (Flat Cast) u t0) (THead +(Bind Abbr) u1 t1))).(let H4 \def (eq_ind T (THead (Flat Cast) u t0) (\lambda +(ee: T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow +False | (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | +(Flat _) \Rightarrow True])])) I (THead (Bind Abbr) u1 t1) H3) in (False_ind +(or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Abbr) +u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (u2: +T).(\lambda (t3: T).(or (pr0 t1 t3) (ex2 T (\lambda (y0: T).(pr0 t1 y0)) +(\lambda (y0: T).(subst0 O u2 y0 t3))))))) (pr0 t1 (lift (S O) O t2))) +H4)))))))) y x H0))) H)))). -theorem pr0_subst0: - \forall (t1: T).(\forall (t2: T).((pr0 t1 t2) \to (\forall (v1: T).(\forall -(w1: T).(\forall (i: nat).((subst0 i v1 t1 w1) \to (\forall (v2: T).((pr0 v1 -v2) \to (or (pr0 w1 t2) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: -T).(subst0 i v2 t2 w2)))))))))))) +lemma pr0_gen_void: + \forall (u1: T).(\forall (t1: T).(\forall (x: T).((pr0 (THead (Bind Void) u1 +t1) x) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T x (THead +(Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda +(_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O x)))))) \def - \lambda (t1: T).(\lambda (t2: T).(\lambda (H: (pr0 t1 t2)).(pr0_ind (\lambda -(t: T).(\lambda (t0: T).(\forall (v1: T).(\forall (w1: T).(\forall (i: -nat).((subst0 i v1 t w1) \to (\forall (v2: T).((pr0 v1 v2) \to (or (pr0 w1 -t0) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 t0 -w2)))))))))))) (\lambda (t: T).(\lambda (v1: T).(\lambda (w1: T).(\lambda (i: -nat).(\lambda (H0: (subst0 i v1 t w1)).(\lambda (v2: T).(\lambda (H1: (pr0 v1 -v2)).(or_intror (pr0 w1 t) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: -T).(subst0 i v2 t w2))) (ex2_sym T (subst0 i v2 t) (pr0 w1) (pr0_subst0_fwd -v1 t w1 i H0 v2 H1)))))))))) (\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) \to (or (pr0 w1 -u2) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 u2 -w2)))))))))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H2: (pr0 t3 -t4)).(\lambda (H3: ((\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 (k: K).(\lambda (v1: T).(\lambda (w1: T).(\lambda (i: -nat).(\lambda (H4: (subst0 i v1 (THead k u1 t3) w1)).(\lambda (v2: -T).(\lambda (H5: (pr0 v1 v2)).(or3_ind (ex2 T (\lambda (u3: T).(eq T w1 -(THead k u3 t3))) (\lambda (u3: T).(subst0 i v1 u1 u3))) (ex2 T (\lambda (t5: -T).(eq T w1 (THead k u1 t5))) (\lambda (t5: T).(subst0 (s k i) v1 t3 t5))) -(ex3_2 T T (\lambda (u3: T).(\lambda (t5: T).(eq T w1 (THead k u3 t5)))) -(\lambda (u3: T).(\lambda (_: T).(subst0 i v1 u1 u3))) (\lambda (_: -T).(\lambda (t5: T).(subst0 (s k i) v1 t3 t5)))) (or (pr0 w1 (THead k u2 t4)) -(ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 (THead k -u2 t4) w2)))) (\lambda (H6: (ex2 T (\lambda (u3: T).(eq T w1 (THead k u3 -t3))) (\lambda (u3: T).(subst0 i v1 u1 u3)))).(ex2_ind T (\lambda (u3: T).(eq -T w1 (THead k u3 t3))) (\lambda (u3: T).(subst0 i v1 u1 u3)) (or (pr0 w1 -(THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: -T).(subst0 i v2 (THead k u2 t4) w2)))) (\lambda (x: T).(\lambda (H7: (eq T w1 -(THead k x t3))).(\lambda (H8: (subst0 i v1 u1 x)).(eq_ind_r T (THead k x t3) -(\lambda (t: T).(or (pr0 t (THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 t -w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 t4) w2))))) (or_ind (pr0 x u2) -(ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 i v2 u2 w2))) -(or (pr0 (THead k x t3) (THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead -k x t3) w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 t4) w2)))) (\lambda -(H9: (pr0 x u2)).(or_introl (pr0 (THead k x t3) (THead k u2 t4)) (ex2 T -(\lambda (w2: T).(pr0 (THead k x t3) w2)) (\lambda (w2: T).(subst0 i v2 -(THead k u2 t4) w2))) (pr0_comp x u2 H9 t3 t4 H2 k))) (\lambda (H9: (ex2 T -(\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 i v2 u2 w2)))).(ex2_ind -T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 i v2 u2 w2)) (or (pr0 -(THead k x t3) (THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead k x t3) -w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 t4) w2)))) (\lambda (x0: -T).(\lambda (H10: (pr0 x x0)).(\lambda (H11: (subst0 i v2 u2 x0)).(or_intror -(pr0 (THead k x t3) (THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead k x -t3) w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 t4) w2))) (ex_intro2 T -(\lambda (w2: T).(pr0 (THead k x t3) w2)) (\lambda (w2: T).(subst0 i v2 -(THead k u2 t4) w2)) (THead k x0 t4) (pr0_comp x x0 H10 t3 t4 H2 k) -(subst0_fst v2 x0 u2 i H11 t4 k)))))) H9)) (H1 v1 x i H8 v2 H5)) w1 H7)))) -H6)) (\lambda (H6: (ex2 T (\lambda (t5: T).(eq T w1 (THead k u1 t5))) -(\lambda (t5: T).(subst0 (s k i) v1 t3 t5)))).(ex2_ind T (\lambda (t5: T).(eq -T w1 (THead k u1 t5))) (\lambda (t5: T).(subst0 (s k i) v1 t3 t5)) (or (pr0 -w1 (THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: -T).(subst0 i v2 (THead k u2 t4) w2)))) (\lambda (x: T).(\lambda (H7: (eq T w1 -(THead k u1 x))).(\lambda (H8: (subst0 (s k i) v1 t3 x)).(eq_ind_r T (THead k -u1 x) (\lambda (t: T).(or (pr0 t (THead k u2 t4)) (ex2 T (\lambda (w2: -T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 t4) w2))))) (or_ind -(pr0 x t4) (ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s k -i) v2 t4 w2))) (or (pr0 (THead k u1 x) (THead k u2 t4)) (ex2 T (\lambda (w2: -T).(pr0 (THead k u1 x) w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 t4) -w2)))) (\lambda (H9: (pr0 x t4)).(or_introl (pr0 (THead k u1 x) (THead k u2 -t4)) (ex2 T (\lambda (w2: T).(pr0 (THead k u1 x) w2)) (\lambda (w2: -T).(subst0 i v2 (THead k u2 t4) w2))) (pr0_comp u1 u2 H0 x t4 H9 k))) -(\lambda (H9: (ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s -k i) v2 t4 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: -T).(subst0 (s k i) v2 t4 w2)) (or (pr0 (THead k u1 x) (THead k u2 t4)) (ex2 T -(\lambda (w2: T).(pr0 (THead k u1 x) w2)) (\lambda (w2: T).(subst0 i v2 -(THead k u2 t4) w2)))) (\lambda (x0: T).(\lambda (H10: (pr0 x x0)).(\lambda -(H11: (subst0 (s k i) v2 t4 x0)).(or_intror (pr0 (THead k u1 x) (THead k u2 -t4)) (ex2 T (\lambda (w2: T).(pr0 (THead k u1 x) w2)) (\lambda (w2: -T).(subst0 i v2 (THead k u2 t4) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 -(THead k u1 x) w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 t4) w2)) (THead -k u2 x0) (pr0_comp u1 u2 H0 x x0 H10 k) (subst0_snd k v2 x0 t4 i H11 u2)))))) -H9)) (H3 v1 x (s k i) H8 v2 H5)) w1 H7)))) H6)) (\lambda (H6: (ex3_2 T T -(\lambda (u3: T).(\lambda (t5: T).(eq T w1 (THead k u3 t5)))) (\lambda (u3: -T).(\lambda (_: T).(subst0 i v1 u1 u3))) (\lambda (_: T).(\lambda (t5: -T).(subst0 (s k i) v1 t3 t5))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda -(t5: T).(eq T w1 (THead k u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 -i v1 u1 u3))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s k i) v1 t3 t5))) -(or (pr0 w1 (THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda -(w2: T).(subst0 i v2 (THead k u2 t4) w2)))) (\lambda (x0: T).(\lambda (x1: -T).(\lambda (H7: (eq T w1 (THead k x0 x1))).(\lambda (H8: (subst0 i v1 u1 -x0)).(\lambda (H9: (subst0 (s k i) v1 t3 x1)).(eq_ind_r T (THead k x0 x1) -(\lambda (t: T).(or (pr0 t (THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 t -w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 t4) w2))))) (or_ind (pr0 x1 -t4) (ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda (w2: T).(subst0 (s k i) v2 -t4 w2))) (or (pr0 (THead k x0 x1) (THead k u2 t4)) (ex2 T (\lambda (w2: -T).(pr0 (THead k x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 t4) -w2)))) (\lambda (H10: (pr0 x1 t4)).(or_ind (pr0 x0 u2) (ex2 T (\lambda (w2: -T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v2 u2 w2))) (or (pr0 (THead k x0 -x1) (THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead k x0 x1) w2)) -(\lambda (w2: T).(subst0 i v2 (THead k u2 t4) w2)))) (\lambda (H11: (pr0 x0 -u2)).(or_introl (pr0 (THead k x0 x1) (THead k u2 t4)) (ex2 T (\lambda (w2: -T).(pr0 (THead k x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 t4) -w2))) (pr0_comp x0 u2 H11 x1 t4 H10 k))) (\lambda (H11: (ex2 T (\lambda (w2: -T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v2 u2 w2)))).(ex2_ind T (\lambda -(w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v2 u2 w2)) (or (pr0 (THead k -x0 x1) (THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead k x0 x1) w2)) -(\lambda (w2: T).(subst0 i v2 (THead k u2 t4) w2)))) (\lambda (x: T).(\lambda -(H12: (pr0 x0 x)).(\lambda (H13: (subst0 i v2 u2 x)).(or_intror (pr0 (THead k -x0 x1) (THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead k x0 x1) w2)) -(\lambda (w2: T).(subst0 i v2 (THead k u2 t4) w2))) (ex_intro2 T (\lambda -(w2: T).(pr0 (THead k x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 -t4) w2)) (THead k x t4) (pr0_comp x0 x H12 x1 t4 H10 k) (subst0_fst v2 x u2 i -H13 t4 k)))))) H11)) (H1 v1 x0 i H8 v2 H5))) (\lambda (H10: (ex2 T (\lambda -(w2: T).(pr0 x1 w2)) (\lambda (w2: T).(subst0 (s k i) v2 t4 w2)))).(ex2_ind T -(\lambda (w2: T).(pr0 x1 w2)) (\lambda (w2: T).(subst0 (s k i) v2 t4 w2)) (or -(pr0 (THead k x0 x1) (THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead k -x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 t4) w2)))) (\lambda (x: -T).(\lambda (H11: (pr0 x1 x)).(\lambda (H12: (subst0 (s k i) v2 t4 -x)).(or_ind (pr0 x0 u2) (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: -T).(subst0 i v2 u2 w2))) (or (pr0 (THead k x0 x1) (THead k u2 t4)) (ex2 T -(\lambda (w2: T).(pr0 (THead k x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 -(THead k u2 t4) w2)))) (\lambda (H13: (pr0 x0 u2)).(or_intror (pr0 (THead k -x0 x1) (THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead k x0 x1) w2)) -(\lambda (w2: T).(subst0 i v2 (THead k u2 t4) w2))) (ex_intro2 T (\lambda -(w2: T).(pr0 (THead k x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 -t4) w2)) (THead k u2 x) (pr0_comp x0 u2 H13 x1 x H11 k) (subst0_snd k v2 x t4 -i H12 u2)))) (\lambda (H13: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda -(w2: T).(subst0 i v2 u2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) -(\lambda (w2: T).(subst0 i v2 u2 w2)) (or (pr0 (THead k x0 x1) (THead k u2 -t4)) (ex2 T (\lambda (w2: T).(pr0 (THead k x0 x1) w2)) (\lambda (w2: -T).(subst0 i v2 (THead k u2 t4) w2)))) (\lambda (x2: T).(\lambda (H14: (pr0 -x0 x2)).(\lambda (H15: (subst0 i v2 u2 x2)).(or_intror (pr0 (THead k x0 x1) -(THead k u2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead k x0 x1) w2)) (\lambda -(w2: T).(subst0 i v2 (THead k u2 t4) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 -(THead k x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 (THead k u2 t4) w2)) -(THead k x2 x) (pr0_comp x0 x2 H14 x1 x H11 k) (subst0_both v2 u2 x2 i H15 k -t4 x H12)))))) H13)) (H1 v1 x0 i H8 v2 H5))))) H10)) (H3 v1 x1 (s k i) H9 v2 -H5)) w1 H7)))))) H6)) (subst0_gen_head k v1 u1 t3 w1 i H4))))))))))))))))) -(\lambda (u: T).(\lambda (v1: T).(\lambda (v2: T).(\lambda (H0: (pr0 v1 -v2)).(\lambda (H1: ((\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 v4 v2 -w2)))))))))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda (H2: (pr0 t3 -t4)).(\lambda (H3: ((\forall (v3: T).(\forall (w1: T).(\forall (i: -nat).((subst0 i v3 t3 w1) \to (\forall (v4: T).((pr0 v3 v4) \to (or (pr0 w1 -t4) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v4 t4 -w2)))))))))))).(\lambda (v0: T).(\lambda (w1: T).(\lambda (i: nat).(\lambda -(H4: (subst0 i v0 (THead (Flat Appl) v1 (THead (Bind Abst) u t3)) -w1)).(\lambda (v3: T).(\lambda (H5: (pr0 v0 v3)).(or3_ind (ex2 T (\lambda -(u2: T).(eq T w1 (THead (Flat Appl) u2 (THead (Bind Abst) u t3)))) (\lambda -(u2: T).(subst0 i v0 v1 u2))) (ex2 T (\lambda (t5: T).(eq T w1 (THead (Flat -Appl) v1 t5))) (\lambda (t5: T).(subst0 (s (Flat Appl) i) v0 (THead (Bind -Abst) u t3) t5))) (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)))) (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 (H6: (ex2 T (\lambda (u2: T).(eq T w1 (THead -(Flat Appl) u2 (THead (Bind Abst) u t3)))) (\lambda (u2: T).(subst0 i v0 v1 -u2)))).(ex2_ind T (\lambda (u2: T).(eq T w1 (THead (Flat Appl) u2 (THead -(Bind Abst) u t3)))) (\lambda (u2: T).(subst0 i v0 v1 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 -(H7: (eq T w1 (THead (Flat Appl) x (THead (Bind Abst) u t3)))).(\lambda (H8: -(subst0 i v0 v1 x)).(eq_ind_r T (THead (Flat Appl) x (THead (Bind Abst) u -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 x v2) (ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: -T).(subst0 i v3 v2 w2))) (or (pr0 (THead (Flat Appl) x (THead (Bind Abst) u -t3)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 (THead (Flat -Appl) x (THead (Bind Abst) u t3)) w2)) (\lambda (w2: T).(subst0 i v3 (THead -(Bind Abbr) v2 t4) w2)))) (\lambda (H9: (pr0 x v2)).(or_introl (pr0 (THead -(Flat Appl) x (THead (Bind Abst) u t3)) (THead (Bind Abbr) v2 t4)) (ex2 T -(\lambda (w2: T).(pr0 (THead (Flat Appl) x (THead (Bind Abst) u t3)) w2)) -(\lambda (w2: T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))) (pr0_beta u x -v2 H9 t3 t4 H2))) (\lambda (H9: (ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda -(w2: T).(subst0 i v3 v2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x w2)) -(\lambda (w2: T).(subst0 i v3 v2 w2)) (or (pr0 (THead (Flat Appl) x (THead -(Bind Abst) u t3)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: T).(pr0 -(THead (Flat Appl) x (THead (Bind Abst) u t3)) w2)) (\lambda (w2: T).(subst0 -i v3 (THead (Bind Abbr) v2 t4) w2)))) (\lambda (x0: T).(\lambda (H10: (pr0 x -x0)).(\lambda (H11: (subst0 i v3 v2 x0)).(or_intror (pr0 (THead (Flat Appl) x -(THead (Bind Abst) u t3)) (THead (Bind Abbr) v2 t4)) (ex2 T (\lambda (w2: -T).(pr0 (THead (Flat Appl) x (THead (Bind Abst) u t3)) w2)) (\lambda (w2: -T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2))) (ex_intro2 T (\lambda (w2: -T).(pr0 (THead (Flat Appl) x (THead (Bind Abst) u t3)) w2)) (\lambda (w2: -T).(subst0 i v3 (THead (Bind Abbr) v2 t4) w2)) (THead (Bind Abbr) x0 t4) -(pr0_beta u x x0 H10 t3 t4 H2) (subst0_fst v3 x0 v2 i H11 t4 (Bind -Abbr))))))) H9)) (H1 v0 x i H8 v3 H5)) w1 H7)))) H6)) (\lambda (H6: (ex2 T -(\lambda (t5: T).(eq T w1 (THead (Flat Appl) v1 t5))) (\lambda (t5: -T).(subst0 (s (Flat Appl) i) v0 (THead (Bind Abst) u t3) t5)))).(ex2_ind T -(\lambda (t5: T).(eq T w1 (THead (Flat Appl) v1 t5))) (\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 (x: T).(\lambda -(H7: (eq T w1 (THead (Flat Appl) v1 x))).(\lambda (H8: (subst0 (s (Flat Appl) -i) v0 (THead (Bind Abst) u t3) x)).(or3_ind (ex2 T (\lambda (u2: T).(eq T x -(THead (Bind Abst) u2 t3))) (\lambda (u2: T).(subst0 (s (Flat Appl) i) v0 u -u2))) (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))) (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)))) (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 (H9: (ex2 T (\lambda (u2: T).(eq T x (THead (Bind Abst) u2 t3))) -(\lambda (u2: T).(subst0 (s (Flat Appl) i) v0 u u2)))).(ex2_ind T (\lambda -(u2: T).(eq T x (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 (x0: T).(\lambda (H10: (eq T x (THead (Bind Abst) x0 -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 (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))) (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 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 (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) 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 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))) (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)).(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 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 (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 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 (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 (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 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 (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 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 -(\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 (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)).(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 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))) (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 (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 -(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 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 (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 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 v4 v2 w2)))))))))))).(\lambda -(u1: T).(\lambda (u2: T).(\lambda (H3: (pr0 u1 u2)).(\lambda (H4: ((\forall -(v3: T).(\forall (w1: T).(\forall (i: nat).((subst0 i v3 u1 w1) \to (\forall -(v4: T).((pr0 v3 v4) \to (or (pr0 w1 u2) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) -(\lambda (w2: T).(subst0 i v4 u2 w2)))))))))))).(\lambda (t3: T).(\lambda -(t4: T).(\lambda (H5: (pr0 t3 t4)).(\lambda (H6: ((\forall (v3: T).(\forall -(w1: T).(\forall (i: nat).((subst0 i v3 t3 w1) \to (\forall (v4: T).((pr0 v3 -v4) \to (or (pr0 w1 t4) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: -T).(subst0 i v4 t4 w2)))))))))))).(\lambda (v0: T).(\lambda (w1: T).(\lambda -(i: nat).(\lambda (H7: (subst0 i v0 (THead (Flat Appl) v1 (THead (Bind b) u1 -t3)) w1)).(\lambda (v3: T).(\lambda (H8: (pr0 v0 v3)).(or3_ind (ex2 T -(\lambda (u3: T).(eq T w1 (THead (Flat Appl) u3 (THead (Bind b) u1 t3)))) -(\lambda (u3: T).(subst0 i v0 v1 u3))) (ex2 T (\lambda (t5: T).(eq T w1 -(THead (Flat Appl) v1 t5))) (\lambda (t5: T).(subst0 (s (Flat Appl) i) v0 -(THead (Bind b) u1 t3) t5))) (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)))) (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 (H9: (ex2 T (\lambda (u3: T).(eq T w1 (THead (Flat Appl) -u3 (THead (Bind b) u1 t3)))) (\lambda (u3: T).(subst0 i v0 v1 u3)))).(ex2_ind -T (\lambda (u3: T).(eq T w1 (THead (Flat Appl) u3 (THead (Bind b) u1 t3)))) -(\lambda (u3: T).(subst0 i v0 v1 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 (H10: (eq T w1 (THead (Flat -Appl) x (THead (Bind b) u1 t3)))).(\lambda (H11: (subst0 i v0 v1 -x)).(eq_ind_r T (THead (Flat Appl) x (THead (Bind b) u1 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 x -v2) (ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 i v3 v2 -w2))) (or (pr0 (THead (Flat Appl) x (THead (Bind b) u1 t3)) (THead (Bind b) -u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 -(THead (Flat Appl) x (THead (Bind b) u1 t3)) w2)) (\lambda (w2: T).(subst0 i -v3 (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4)) w2)))) -(\lambda (H12: (pr0 x v2)).(or_introl (pr0 (THead (Flat Appl) x (THead (Bind -b) u1 t3)) (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 -T (\lambda (w2: T).(pr0 (THead (Flat Appl) x (THead (Bind b) u1 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 x v2 H12 u1 u2 H3 t3 t4 H5))) (\lambda -(H12: (ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 i v3 v2 -w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 i v3 -v2 w2)) (or (pr0 (THead (Flat Appl) x (THead (Bind b) u1 t3)) (THead (Bind b) -u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: T).(pr0 -(THead (Flat Appl) x (THead (Bind b) u1 t3)) 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: (pr0 x x0)).(\lambda (H14: (subst0 i v3 v2 -x0)).(or_intror (pr0 (THead (Flat Appl) x (THead (Bind b) u1 t3)) (THead -(Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t4))) (ex2 T (\lambda (w2: -T).(pr0 (THead (Flat Appl) x (THead (Bind b) u1 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) x (THead (Bind b) -u1 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 x0) t4)) (pr0_upsilon b H0 x x0 H13 u1 u2 H3 t3 t4 H5) (subst0_snd -(Bind b) v3 (THead (Flat Appl) (lift (S O) O x0) t4) (THead (Flat Appl) (lift -(S O) O v2) t4) i (subst0_fst v3 (lift (S O) O x0) (lift (S O) O v2) (s (Bind -b) i) (subst0_lift_ge_s v2 x0 v3 i H14 O (le_O_n i) b) t4 (Flat Appl)) -u2)))))) H12)) (H2 v0 x i H11 v3 H8)) w1 H10)))) H9)) (\lambda (H9: (ex2 T -(\lambda (t5: T).(eq T w1 (THead (Flat Appl) v1 t5))) (\lambda (t5: -T).(subst0 (s (Flat Appl) i) v0 (THead (Bind b) u1 t3) t5)))).(ex2_ind T -(\lambda (t5: T).(eq T w1 (THead (Flat Appl) v1 t5))) (\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 (x: T).(\lambda (H10: (eq -T w1 (THead (Flat Appl) v1 x))).(\lambda (H11: (subst0 (s (Flat Appl) i) v0 -(THead (Bind b) u1 t3) x)).(or3_ind (ex2 T (\lambda (u3: T).(eq T x (THead -(Bind b) u3 t3))) (\lambda (u3: T).(subst0 (s (Flat Appl) i) v0 u1 u3))) (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))) (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)))) (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 (H12: (ex2 T -(\lambda (u3: T).(eq T x (THead (Bind b) u3 t3))) (\lambda (u3: T).(subst0 (s -(Flat Appl) i) v0 u1 u3)))).(ex2_ind T (\lambda (u3: T).(eq T x (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 (x0: T).(\lambda (H13: (eq -T x (THead (Bind b) x0 t3))).(\lambda (H14: (subst0 (s (Flat Appl) i) v0 u1 -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 (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)))).(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 (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 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 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 -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 -(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)).(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)))) (\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))) (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 (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) 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 (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))))) (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 (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 (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 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 (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 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 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 (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 (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: -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) x2 (THead (Flat Appl) (lift -(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 (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: -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) x2 (THead (Flat Appl) (lift -(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 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 (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 (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))) (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 -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) 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 (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: -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 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 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 -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 (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)).(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)))) (\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 (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 (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 (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) x (THead (Flat Appl) (lift -(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 (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) x (THead (Flat Appl) (lift -(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 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 (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 (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 (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 -(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 v2) -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) 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 (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 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 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 (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 (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 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) 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 (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: -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 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 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) -\to (or (pr0 w1 u2) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: -T).(subst0 i v2 u2 w2)))))))))))).(\lambda (t3: T).(\lambda (t4: T).(\lambda -(H2: (pr0 t3 t4)).(\lambda (H3: ((\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 (w: T).(\lambda (H4: (subst0 O u2 t4 w)).(\lambda -(v1: T).(\lambda (w1: T).(\lambda (i: nat).(\lambda (H5: (subst0 i v1 (THead -(Bind Abbr) u1 t3) w1)).(\lambda (v2: T).(\lambda (H6: (pr0 v1 v2)).(or3_ind -(ex2 T (\lambda (u3: T).(eq T w1 (THead (Bind Abbr) u3 t3))) (\lambda (u3: -T).(subst0 i v1 u1 u3))) (ex2 T (\lambda (t5: T).(eq T w1 (THead (Bind Abbr) -u1 t5))) (\lambda (t5: T).(subst0 (s (Bind Abbr) i) v1 t3 t5))) (ex3_2 T T -(\lambda (u3: T).(\lambda (t5: T).(eq T w1 (THead (Bind Abbr) u3 t5)))) -(\lambda (u3: T).(\lambda (_: T).(subst0 i v1 u1 u3))) (\lambda (_: -T).(\lambda (t5: T).(subst0 (s (Bind Abbr) i) v1 t3 t5)))) (or (pr0 w1 (THead -(Bind Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: -T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2)))) (\lambda (H7: (ex2 T (\lambda -(u3: T).(eq T w1 (THead (Bind Abbr) u3 t3))) (\lambda (u3: T).(subst0 i v1 u1 -u3)))).(ex2_ind T (\lambda (u3: T).(eq T w1 (THead (Bind Abbr) u3 t3))) -(\lambda (u3: T).(subst0 i v1 u1 u3)) (or (pr0 w1 (THead (Bind Abbr) u2 w)) -(ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i v2 (THead -(Bind Abbr) u2 w) w2)))) (\lambda (x: T).(\lambda (H8: (eq T w1 (THead (Bind -Abbr) x t3))).(\lambda (H9: (subst0 i v1 u1 x)).(eq_ind_r T (THead (Bind -Abbr) x t3) (\lambda (t: T).(or (pr0 t (THead (Bind Abbr) u2 w)) (ex2 T -(\lambda (w2: T).(pr0 t w2)) (\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) -u2 w) w2))))) (or_ind (pr0 x u2) (ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda -(w2: T).(subst0 i v2 u2 w2))) (or (pr0 (THead (Bind Abbr) x t3) (THead (Bind -Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) x t3) w2)) -(\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2)))) (\lambda (H10: -(pr0 x u2)).(or_introl (pr0 (THead (Bind Abbr) x t3) (THead (Bind Abbr) u2 -w)) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) x t3) w2)) (\lambda (w2: -T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2))) (pr0_delta x u2 H10 t3 t4 H2 w -H4))) (\lambda (H10: (ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: -T).(subst0 i v2 u2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x w2)) (\lambda -(w2: T).(subst0 i v2 u2 w2)) (or (pr0 (THead (Bind Abbr) x t3) (THead (Bind -Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) x t3) w2)) -(\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2)))) (\lambda (x0: -T).(\lambda (H11: (pr0 x x0)).(\lambda (H12: (subst0 i v2 u2 x0)).(ex2_ind T -(\lambda (t: T).(subst0 O x0 t4 t)) (\lambda (t: T).(subst0 (S (plus i O)) v2 -w t)) (or (pr0 (THead (Bind Abbr) x t3) (THead (Bind Abbr) u2 w)) (ex2 T -(\lambda (w2: T).(pr0 (THead (Bind Abbr) x t3) w2)) (\lambda (w2: T).(subst0 -i v2 (THead (Bind Abbr) u2 w) w2)))) (\lambda (x1: T).(\lambda (H13: (subst0 -O x0 t4 x1)).(\lambda (H14: (subst0 (S (plus i O)) v2 w x1)).(let H15 \def -(f_equal nat nat S (plus i O) i (sym_eq nat i (plus i O) (plus_n_O i))) in -(let H16 \def (eq_ind nat (S (plus i O)) (\lambda (n: nat).(subst0 n v2 w -x1)) H14 (S i) H15) in (or_intror (pr0 (THead (Bind Abbr) x t3) (THead (Bind -Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) x t3) w2)) -(\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2))) (ex_intro2 T -(\lambda (w2: T).(pr0 (THead (Bind Abbr) x t3) w2)) (\lambda (w2: T).(subst0 -i v2 (THead (Bind Abbr) u2 w) w2)) (THead (Bind Abbr) x0 x1) (pr0_delta x x0 -H11 t3 t4 H2 x1 H13) (subst0_both v2 u2 x0 i H12 (Bind Abbr) w x1 H16)))))))) -(subst0_subst0_back t4 w u2 O H4 x0 v2 i H12))))) H10)) (H1 v1 x i H9 v2 H6)) -w1 H8)))) H7)) (\lambda (H7: (ex2 T (\lambda (t5: T).(eq T w1 (THead (Bind -Abbr) u1 t5))) (\lambda (t5: T).(subst0 (s (Bind Abbr) i) v1 t3 -t5)))).(ex2_ind T (\lambda (t5: T).(eq T w1 (THead (Bind Abbr) u1 t5))) -(\lambda (t5: T).(subst0 (s (Bind Abbr) i) v1 t3 t5)) (or (pr0 w1 (THead -(Bind Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: -T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2)))) (\lambda (x: T).(\lambda (H8: -(eq T w1 (THead (Bind Abbr) u1 x))).(\lambda (H9: (subst0 (s (Bind Abbr) i) -v1 t3 x)).(eq_ind_r T (THead (Bind Abbr) u1 x) (\lambda (t: T).(or (pr0 t -(THead (Bind Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda (w2: -T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2))))) (or_ind (pr0 x t4) (ex2 T -(\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Bind Abbr) i) v2 t4 -w2))) (or (pr0 (THead (Bind Abbr) u1 x) (THead (Bind Abbr) u2 w)) (ex2 T -(\lambda (w2: T).(pr0 (THead (Bind Abbr) u1 x) w2)) (\lambda (w2: T).(subst0 -i v2 (THead (Bind Abbr) u2 w) w2)))) (\lambda (H10: (pr0 x t4)).(or_introl -(pr0 (THead (Bind Abbr) u1 x) (THead (Bind Abbr) u2 w)) (ex2 T (\lambda (w2: -T).(pr0 (THead (Bind Abbr) u1 x) w2)) (\lambda (w2: T).(subst0 i v2 (THead -(Bind Abbr) u2 w) w2))) (pr0_delta u1 u2 H0 x t4 H10 w H4))) (\lambda (H10: -(ex2 T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: T).(subst0 (s (Bind Abbr) -i) v2 t4 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x w2)) (\lambda (w2: -T).(subst0 (s (Bind Abbr) i) v2 t4 w2)) (or (pr0 (THead (Bind Abbr) u1 x) -(THead (Bind Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) u1 -x) w2)) (\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2)))) -(\lambda (x0: T).(\lambda (H11: (pr0 x x0)).(\lambda (H12: (subst0 (s (Bind -Abbr) i) v2 t4 x0)).(ex2_ind T (\lambda (t: T).(subst0 O u2 x0 t)) (\lambda -(t: T).(subst0 (s (Bind Abbr) i) v2 w t)) (or (pr0 (THead (Bind Abbr) u1 x) -(THead (Bind Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) u1 -x) w2)) (\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2)))) -(\lambda (x1: T).(\lambda (H13: (subst0 O u2 x0 x1)).(\lambda (H14: (subst0 -(s (Bind Abbr) i) v2 w x1)).(or_intror (pr0 (THead (Bind Abbr) u1 x) (THead -(Bind Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) u1 x) w2)) -(\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2))) (ex_intro2 T -(\lambda (w2: T).(pr0 (THead (Bind Abbr) u1 x) w2)) (\lambda (w2: T).(subst0 -i v2 (THead (Bind Abbr) u2 w) w2)) (THead (Bind Abbr) u2 x1) (pr0_delta u1 u2 -H0 x x0 H11 x1 H13) (subst0_snd (Bind Abbr) v2 x1 w i H14 u2)))))) -(subst0_confluence_neq t4 x0 v2 (s (Bind Abbr) i) H12 w u2 O H4 (sym_not_eq -nat O (S i) (O_S i))))))) H10)) (H3 v1 x (s (Bind Abbr) i) H9 v2 H6)) w1 -H8)))) H7)) (\lambda (H7: (ex3_2 T T (\lambda (u3: T).(\lambda (t5: T).(eq T -w1 (THead (Bind Abbr) u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i v1 -u1 u3))) (\lambda (_: T).(\lambda (t5: T).(subst0 (s (Bind Abbr) i) v1 t3 -t5))))).(ex3_2_ind T T (\lambda (u3: T).(\lambda (t5: T).(eq T w1 (THead -(Bind Abbr) u3 t5)))) (\lambda (u3: T).(\lambda (_: T).(subst0 i v1 u1 u3))) -(\lambda (_: T).(\lambda (t5: T).(subst0 (s (Bind Abbr) i) v1 t3 t5))) (or -(pr0 w1 (THead (Bind Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) -(\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2)))) (\lambda (x0: -T).(\lambda (x1: T).(\lambda (H8: (eq T w1 (THead (Bind Abbr) x0 -x1))).(\lambda (H9: (subst0 i v1 u1 x0)).(\lambda (H10: (subst0 (s (Bind -Abbr) i) v1 t3 x1)).(eq_ind_r T (THead (Bind Abbr) x0 x1) (\lambda (t: T).(or -(pr0 t (THead (Bind Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 t w2)) (\lambda -(w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2))))) (or_ind (pr0 x1 t4) -(ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda (w2: T).(subst0 (s (Bind Abbr) -i) v2 t4 w2))) (or (pr0 (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 w)) -(ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) x0 x1) w2)) (\lambda (w2: -T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2)))) (\lambda (H11: (pr0 x1 -t4)).(or_ind (pr0 x0 u2) (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: -T).(subst0 i v2 u2 w2))) (or (pr0 (THead (Bind Abbr) x0 x1) (THead (Bind -Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) x0 x1) w2)) -(\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2)))) (\lambda (H12: -(pr0 x0 u2)).(or_introl (pr0 (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 -w)) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) x0 x1) w2)) (\lambda (w2: -T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2))) (pr0_delta x0 u2 H12 x1 t4 H11 -w H4))) (\lambda (H12: (ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: -T).(subst0 i v2 u2 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda -(w2: T).(subst0 i v2 u2 w2)) (or (pr0 (THead (Bind Abbr) x0 x1) (THead (Bind -Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) x0 x1) w2)) -(\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2)))) (\lambda (x: -T).(\lambda (H13: (pr0 x0 x)).(\lambda (H14: (subst0 i v2 u2 x)).(ex2_ind T -(\lambda (t: T).(subst0 O x t4 t)) (\lambda (t: T).(subst0 (S (plus i O)) v2 -w t)) (or (pr0 (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 w)) (ex2 T -(\lambda (w2: T).(pr0 (THead (Bind Abbr) x0 x1) w2)) (\lambda (w2: T).(subst0 -i v2 (THead (Bind Abbr) u2 w) w2)))) (\lambda (x2: T).(\lambda (H15: (subst0 -O x t4 x2)).(\lambda (H16: (subst0 (S (plus i O)) v2 w x2)).(let H17 \def -(f_equal nat nat S (plus i O) i (sym_eq nat i (plus i O) (plus_n_O i))) in -(let H18 \def (eq_ind nat (S (plus i O)) (\lambda (n: nat).(subst0 n v2 w -x2)) H16 (S i) H17) in (or_intror (pr0 (THead (Bind Abbr) x0 x1) (THead (Bind -Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) x0 x1) w2)) -(\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2))) (ex_intro2 T -(\lambda (w2: T).(pr0 (THead (Bind Abbr) x0 x1) w2)) (\lambda (w2: T).(subst0 -i v2 (THead (Bind Abbr) u2 w) w2)) (THead (Bind Abbr) x x2) (pr0_delta x0 x -H13 x1 t4 H11 x2 H15) (subst0_both v2 u2 x i H14 (Bind Abbr) w x2 H18)))))))) -(subst0_subst0_back t4 w u2 O H4 x v2 i H14))))) H12)) (H1 v1 x0 i H9 v2 -H6))) (\lambda (H11: (ex2 T (\lambda (w2: T).(pr0 x1 w2)) (\lambda (w2: -T).(subst0 (s (Bind Abbr) i) v2 t4 w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x1 -w2)) (\lambda (w2: T).(subst0 (s (Bind Abbr) i) v2 t4 w2)) (or (pr0 (THead -(Bind Abbr) x0 x1) (THead (Bind Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 -(THead (Bind Abbr) x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 (THead (Bind -Abbr) u2 w) w2)))) (\lambda (x: T).(\lambda (H12: (pr0 x1 x)).(\lambda (H13: -(subst0 (s (Bind Abbr) i) v2 t4 x)).(or_ind (pr0 x0 u2) (ex2 T (\lambda (w2: -T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v2 u2 w2))) (or (pr0 (THead (Bind -Abbr) x0 x1) (THead (Bind Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 (THead -(Bind Abbr) x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 -w) w2)))) (\lambda (H14: (pr0 x0 u2)).(ex2_ind T (\lambda (t: T).(subst0 O u2 -x t)) (\lambda (t: T).(subst0 (s (Bind Abbr) i) v2 w t)) (or (pr0 (THead -(Bind Abbr) x0 x1) (THead (Bind Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 -(THead (Bind Abbr) x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 (THead (Bind -Abbr) u2 w) w2)))) (\lambda (x2: T).(\lambda (H15: (subst0 O u2 x -x2)).(\lambda (H16: (subst0 (s (Bind Abbr) i) v2 w x2)).(or_intror (pr0 -(THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 w)) (ex2 T (\lambda (w2: -T).(pr0 (THead (Bind Abbr) x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 (THead -(Bind Abbr) u2 w) w2))) (ex_intro2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) -x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2)) -(THead (Bind Abbr) u2 x2) (pr0_delta x0 u2 H14 x1 x H12 x2 H15) (subst0_snd -(Bind Abbr) v2 x2 w i H16 u2)))))) (subst0_confluence_neq t4 x v2 (s (Bind -Abbr) i) H13 w u2 O H4 (sym_not_eq nat O (S i) (O_S i))))) (\lambda (H14: -(ex2 T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v2 u2 -w2)))).(ex2_ind T (\lambda (w2: T).(pr0 x0 w2)) (\lambda (w2: T).(subst0 i v2 -u2 w2)) (or (pr0 (THead (Bind Abbr) x0 x1) (THead (Bind Abbr) u2 w)) (ex2 T -(\lambda (w2: T).(pr0 (THead (Bind Abbr) x0 x1) w2)) (\lambda (w2: T).(subst0 -i v2 (THead (Bind Abbr) u2 w) w2)))) (\lambda (x2: T).(\lambda (H15: (pr0 x0 -x2)).(\lambda (H16: (subst0 i v2 u2 x2)).(ex2_ind T (\lambda (t: T).(subst0 O -x2 t4 t)) (\lambda (t: T).(subst0 (S (plus i O)) v2 w t)) (or (pr0 (THead -(Bind Abbr) x0 x1) (THead (Bind Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 -(THead (Bind Abbr) x0 x1) w2)) (\lambda (w2: T).(subst0 i v2 (THead (Bind -Abbr) u2 w) w2)))) (\lambda (x3: T).(\lambda (H17: (subst0 O x2 t4 -x3)).(\lambda (H18: (subst0 (S (plus i O)) v2 w x3)).(let H19 \def (f_equal -nat nat S (plus i O) i (sym_eq nat i (plus i O) (plus_n_O i))) in (let H20 -\def (eq_ind nat (S (plus i O)) (\lambda (n: nat).(subst0 n v2 w x3)) H18 (S -i) H19) in (ex2_ind T (\lambda (t: T).(subst0 (s (Bind Abbr) i) v2 x3 t)) -(\lambda (t: T).(subst0 O x2 x t)) (or (pr0 (THead (Bind Abbr) x0 x1) (THead -(Bind Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) x0 x1) -w2)) (\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2)))) (\lambda -(x4: T).(\lambda (H21: (subst0 (s (Bind Abbr) i) v2 x3 x4)).(\lambda (H22: -(subst0 O x2 x x4)).(or_intror (pr0 (THead (Bind Abbr) x0 x1) (THead (Bind -Abbr) u2 w)) (ex2 T (\lambda (w2: T).(pr0 (THead (Bind Abbr) x0 x1) w2)) -(\lambda (w2: T).(subst0 i v2 (THead (Bind Abbr) u2 w) w2))) (ex_intro2 T -(\lambda (w2: T).(pr0 (THead (Bind Abbr) x0 x1) w2)) (\lambda (w2: T).(subst0 -i v2 (THead (Bind Abbr) u2 w) w2)) (THead (Bind Abbr) x2 x4) (pr0_delta x0 x2 -H15 x1 x H12 x4 H22) (subst0_both v2 u2 x2 i H16 (Bind Abbr) w x4 -(subst0_trans x3 w v2 (s (Bind Abbr) i) H20 x4 H21))))))) -(subst0_confluence_neq t4 x3 x2 O H17 x v2 (s (Bind Abbr) i) H13 (O_S -i)))))))) (subst0_subst0_back t4 w u2 O H4 x2 v2 i H16))))) H14)) (H1 v1 x0 i -H9 v2 H6))))) H11)) (H3 v1 x1 (s (Bind Abbr) i) H10 v2 H6)) w1 H8)))))) H7)) -(subst0_gen_head (Bind Abbr) v1 u1 t3 w1 i H5)))))))))))))))))) (\lambda (b: -B).(\lambda (H0: (not (eq B b Abst))).(\lambda (t3: T).(\lambda (t4: -T).(\lambda (H1: (pr0 t3 t4)).(\lambda (H2: ((\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 (H3: (subst0 i v1 (THead (Bind b) u (lift -(S O) O t3)) w1)).(\lambda (v2: T).(\lambda (H4: (pr0 v1 v2)).(or3_ind (ex2 T -(\lambda (u2: T).(eq T w1 (THead (Bind b) u2 (lift (S O) O t3)))) (\lambda -(u2: T).(subst0 i v1 u u2))) (ex2 T (\lambda (t5: T).(eq T w1 (THead (Bind b) -u t5))) (\lambda (t5: T).(subst0 (s (Bind b) i) v1 (lift (S O) O t3) t5))) -(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)))) (or -(pr0 w1 t4) (ex2 T (\lambda (w2: T).(pr0 w1 w2)) (\lambda (w2: T).(subst0 i -v2 t4 w2)))) (\lambda (H5: (ex2 T (\lambda (u2: T).(eq T w1 (THead (Bind b) -u2 (lift (S O) O t3)))) (\lambda (u2: T).(subst0 i v1 u u2)))).(ex2_ind T -(\lambda (u2: T).(eq T w1 (THead (Bind b) u2 (lift (S O) O 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 (H6: -(eq T w1 (THead (Bind b) x (lift (S O) O t3)))).(\lambda (_: (subst0 i v1 u -x)).(eq_ind_r T (THead (Bind b) x (lift (S O) O 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 (Bind b) x (lift (S O) O t3)) t4) (ex2 T -(\lambda (w2: T).(pr0 (THead (Bind b) x (lift (S O) O t3)) w2)) (\lambda (w2: -T).(subst0 i v2 t4 w2))) (pr0_zeta b H0 t3 t4 H1 x)) w1 H6)))) H5)) (\lambda -(H5: (ex2 T (\lambda (t5: T).(eq T w1 (THead (Bind b) u t5))) (\lambda (t5: -T).(subst0 (s (Bind b) i) v1 (lift (S O) O t3) t5)))).(ex2_ind T (\lambda -(t5: T).(eq T w1 (THead (Bind b) u t5))) (\lambda (t5: T).(subst0 (s (Bind b) -i) v1 (lift (S O) O 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 (H6: -(eq T w1 (THead (Bind b) u x))).(\lambda (H7: (subst0 (s (Bind b) i) v1 (lift -(S O) O t3) x)).(ex2_ind T (\lambda (t5: T).(eq T x (lift (S O) O 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 (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)).(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 (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 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: -T).(subst0 (s (Bind b) i) v1 (lift (S O) O 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 (x1: T).(\lambda (H6: (eq T w1 (THead (Bind b) x0 -x1))).(\lambda (_: (subst0 i v1 u x0)).(\lambda (H8: (subst0 (s (Bind b) i) -v1 (lift (S O) O t3) x1)).(ex2_ind T (\lambda (t5: T).(eq T x1 (lift (S O) O -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)).(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)))) (\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)) 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_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: -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 (x0: -T).(\lambda (x1: T).(\lambda (H5: (eq T w1 (THead (Flat Cast) x0 -x1))).(\lambda (_: (subst0 i v1 u x0)).(\lambda (H7: (subst0 (s (Flat Cast) -i) v1 t3 x1)).(eq_ind_r T (THead (Flat Cast) 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))))) (or_ind (pr0 x1 t4) (ex2 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 (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_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))) (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))). -(* COMMENTS -Initial nodes: 38857 -END *) + \lambda (u1: T).(\lambda (t1: T).(\lambda (x: T).(\lambda (H: (pr0 (THead +(Bind Void) u1 t1) x)).(insert_eq T (THead (Bind Void) u1 t1) (\lambda (t: +T).(pr0 t x)) (\lambda (_: T).(or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: +T).(eq T x (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 +u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) +O x)))) (\lambda (y: T).(\lambda (H0: (pr0 y x)).(pr0_ind (\lambda (t: +T).(\lambda (t0: T).((eq T t (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T +(\lambda (u2: T).(\lambda (t2: T).(eq T t0 (THead (Bind Void) u2 t2)))) +(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: +T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O t0)))))) (\lambda (t: T).(\lambda +(H1: (eq T t (THead (Bind Void) u1 t1))).(let H2 \def (f_equal T T (\lambda +(e: T).e) t (THead (Bind Void) u1 t1) H1) in (eq_ind_r T (THead (Bind Void) +u1 t1) (\lambda (t0: T).(or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq +T t0 (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 +u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O +t0)))) (or_introl (ex3_2 T T (\lambda (u2: T).(\lambda (t2: T).(eq T (THead +(Bind Void) u1 t1) (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: +T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 +(lift (S O) O (THead (Bind Void) u1 t1))) (ex3_2_intro T T (\lambda (u2: +T).(\lambda (t2: T).(eq T (THead (Bind Void) u1 t1) (THead (Bind Void) u2 +t2)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: +T).(\lambda (t2: T).(pr0 t1 t2))) u1 t1 (refl_equal T (THead (Bind Void) u1 +t1)) (pr0_refl u1) (pr0_refl t1))) t H2)))) (\lambda (u0: T).(\lambda (u2: +T).(\lambda (H1: (pr0 u0 u2)).(\lambda (H2: (((eq T u0 (THead (Bind Void) u1 +t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead +(Bind Void) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda +(_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O +u2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H3: (pr0 t0 +t2)).(\lambda (H4: (((eq T t0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T +(\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u3 t3)))) +(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: +T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (k: K).(\lambda +(H5: (eq T (THead k u0 t0) (THead (Bind Void) u1 t1))).(let H6 \def (f_equal +T K (\lambda (e: T).(match e with [(TSort _) \Rightarrow k | (TLRef _) +\Rightarrow k | (THead k0 _ _) \Rightarrow k0])) (THead k u0 t0) (THead (Bind +Void) u1 t1) H5) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e with +[(TSort _) \Rightarrow u0 | (TLRef _) \Rightarrow u0 | (THead _ t _) +\Rightarrow t])) (THead k u0 t0) (THead (Bind Void) u1 t1) H5) in ((let H8 +\def (f_equal T T (\lambda (e: T).(match e with [(TSort _) \Rightarrow t0 | +(TLRef _) \Rightarrow t0 | (THead _ _ t) \Rightarrow t])) (THead k u0 t0) +(THead (Bind Void) u1 t1) H5) in (\lambda (H9: (eq T u0 u1)).(\lambda (H10: +(eq K k (Bind Void))).(eq_ind_r K (Bind Void) (\lambda (k0: K).(or (ex3_2 T T +(\lambda (u3: T).(\lambda (t3: T).(eq T (THead k0 u2 t2) (THead (Bind Void) +u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: +T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O (THead k0 u2 t2))))) +(let H11 \def (eq_ind T t0 (\lambda (t: T).((eq T t (THead (Bind Void) u1 +t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead +(Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda +(_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O t2))))) H4 t1 +H8) in (let H12 \def (eq_ind T t0 (\lambda (t: T).(pr0 t t2)) H3 t1 H8) in +(let H13 \def (eq_ind T u0 (\lambda (t: T).((eq T t (THead (Bind Void) u1 +t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T u2 (THead +(Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda +(_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O u2))))) H2 u1 +H9) in (let H14 \def (eq_ind T u0 (\lambda (t: T).(pr0 t u2)) H1 u1 H9) in +(or_introl (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind +Void) u2 t2) (THead (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_: +T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 +(lift (S O) O (THead (Bind Void) u2 t2))) (ex3_2_intro T T (\lambda (u3: +T).(\lambda (t3: T).(eq T (THead (Bind Void) u2 t2) (THead (Bind Void) u3 +t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: +T).(\lambda (t3: T).(pr0 t1 t3))) u2 t2 (refl_equal T (THead (Bind Void) u2 +t2)) H14 H12)))))) k H10)))) H7)) H6)))))))))))) (\lambda (u: T).(\lambda +(v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 v2)).(\lambda (_: (((eq T v1 +(THead (Bind Void) u1 t1)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t2: +T).(eq T v2 (THead (Bind Void) u2 t2)))) (\lambda (u2: T).(\lambda (_: +T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 +(lift (S O) O v2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 +t2)).(\lambda (_: (((eq T t0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T +(\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2 t3)))) +(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: +T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (H5: (eq T (THead +(Flat Appl) v1 (THead (Bind Abst) u t0)) (THead (Bind Void) u1 t1))).(let H6 +\def (eq_ind T (THead (Flat Appl) v1 (THead (Bind Abst) u t0)) (\lambda (ee: +T).(match ee with [(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False +| (THead k _ _) \Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat +_) \Rightarrow True])])) I (THead (Bind Void) u1 t1) H5) in (False_ind (or +(ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) v2 t2) +(THead (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) +(\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O (THead +(Bind Abbr) v2 t2)))) H6)))))))))))) (\lambda (b: B).(\lambda (_: (not (eq B +b Abst))).(\lambda (v1: T).(\lambda (v2: T).(\lambda (_: (pr0 v1 +v2)).(\lambda (_: (((eq T v1 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T +(\lambda (u2: T).(\lambda (t2: T).(eq T v2 (THead (Bind Void) u2 t2)))) +(\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t2: +T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O v2)))))).(\lambda (u0: T).(\lambda +(u2: T).(\lambda (_: (pr0 u0 u2)).(\lambda (_: (((eq T u0 (THead (Bind Void) +u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead +(Bind Void) u3 t2)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda +(_: T).(\lambda (t2: T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O +u2)))))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda +(_: (((eq T t0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T (\lambda (u3: +T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u3 t3)))) (\lambda (u3: +T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 +t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (H8: (eq T (THead (Flat Appl) +v1 (THead (Bind b) u0 t0)) (THead (Bind Void) u1 t1))).(let H9 \def (eq_ind T +(THead (Flat Appl) v1 (THead (Bind b) u0 t0)) (\lambda (ee: T).(match ee with +[(TSort _) \Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) +\Rightarrow (match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow +True])])) I (THead (Bind Void) u1 t1) H8) in (False_ind (or (ex3_2 T T +(\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind b) u2 (THead (Flat Appl) +(lift (S O) O v2) t2)) (THead (Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda +(_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 +(lift (S O) O (THead (Bind b) u2 (THead (Flat Appl) (lift (S O) O v2) t2))))) +H9))))))))))))))))) (\lambda (u0: T).(\lambda (u2: T).(\lambda (_: (pr0 u0 +u2)).(\lambda (_: (((eq T u0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T +(\lambda (u3: T).(\lambda (t2: T).(eq T u2 (THead (Bind Void) u3 t2)))) +(\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: T).(\lambda (t2: +T).(pr0 t1 t2)))) (pr0 t1 (lift (S O) O u2)))))).(\lambda (t0: T).(\lambda +(t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: (((eq T t0 (THead (Bind Void) +u1 t1)) \to (or (ex3_2 T T (\lambda (u3: T).(\lambda (t3: T).(eq T t2 (THead +(Bind Void) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda +(_: T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O +t2)))))).(\lambda (w: T).(\lambda (_: (subst0 O u2 t2 w)).(\lambda (H6: (eq T +(THead (Bind Abbr) u0 t0) (THead (Bind Void) u1 t1))).(let H7 \def (eq_ind T +(THead (Bind Abbr) u0 t0) (\lambda (ee: T).(match ee with [(TSort _) +\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow +(match k with [(Bind b) \Rightarrow (match b with [Abbr \Rightarrow True | +Abst \Rightarrow False | Void \Rightarrow False]) | (Flat _) \Rightarrow +False])])) I (THead (Bind Void) u1 t1) H6) in (False_ind (or (ex3_2 T T +(\lambda (u3: T).(\lambda (t3: T).(eq T (THead (Bind Abbr) u2 w) (THead (Bind +Void) u3 t3)))) (\lambda (u3: T).(\lambda (_: T).(pr0 u1 u3))) (\lambda (_: +T).(\lambda (t3: T).(pr0 t1 t3)))) (pr0 t1 (lift (S O) O (THead (Bind Abbr) +u2 w)))) H7))))))))))))) (\lambda (b: B).(\lambda (H1: (not (eq B b +Abst))).(\lambda (t0: T).(\lambda (t2: T).(\lambda (H2: (pr0 t0 t2)).(\lambda +(H3: (((eq T t0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T (\lambda (u2: +T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2 t3)))) (\lambda (u2: +T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 +t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (u: T).(\lambda (H4: (eq T +(THead (Bind b) u (lift (S O) O t0)) (THead (Bind Void) u1 t1))).(let H5 \def +(f_equal T B (\lambda (e: T).(match e with [(TSort _) \Rightarrow b | (TLRef +_) \Rightarrow b | (THead k _ _) \Rightarrow (match k with [(Bind b0) +\Rightarrow b0 | (Flat _) \Rightarrow b])])) (THead (Bind b) u (lift (S O) O +t0)) (THead (Bind Void) u1 t1) H4) in ((let H6 \def (f_equal T T (\lambda (e: +T).(match e with [(TSort _) \Rightarrow u | (TLRef _) \Rightarrow u | (THead +_ t _) \Rightarrow t])) (THead (Bind b) u (lift (S O) O t0)) (THead (Bind +Void) u1 t1) H4) in ((let H7 \def (f_equal T T (\lambda (e: T).(match e with +[(TSort _) \Rightarrow (lref_map (\lambda (x0: nat).(plus x0 (S O))) O t0) | +(TLRef _) \Rightarrow (lref_map (\lambda (x0: nat).(plus x0 (S O))) O t0) | +(THead _ _ t) \Rightarrow t])) (THead (Bind b) u (lift (S O) O t0)) (THead +(Bind Void) u1 t1) H4) in (\lambda (_: (eq T u u1)).(\lambda (H9: (eq B b +Void)).(let H10 \def (eq_ind B b (\lambda (b0: B).(not (eq B b0 Abst))) H1 +Void H9) in (let H11 \def (eq_ind_r T t1 (\lambda (t: T).((eq T t0 (THead +(Bind Void) u1 t)) \to (or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T +t2 (THead (Bind Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 +u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t t3)))) (pr0 t (lift (S O) O +t2))))) H3 (lift (S O) O t0) H7) in (eq_ind T (lift (S O) O t0) (\lambda (t: +T).(or (ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind +Void) u2 t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: +T).(\lambda (t3: T).(pr0 t t3)))) (pr0 t (lift (S O) O t2)))) (or_intror +(ex3_2 T T (\lambda (u2: T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2 +t3)))) (\lambda (u2: T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: +T).(\lambda (t3: T).(pr0 (lift (S O) O t0) t3)))) (pr0 (lift (S O) O t0) +(lift (S O) O t2)) (pr0_lift t0 t2 H2 (S O) O)) t1 H7)))))) H6)) H5)))))))))) +(\lambda (t0: T).(\lambda (t2: T).(\lambda (_: (pr0 t0 t2)).(\lambda (_: +(((eq T t0 (THead (Bind Void) u1 t1)) \to (or (ex3_2 T T (\lambda (u2: +T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2 t3)))) (\lambda (u2: +T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 +t3)))) (pr0 t1 (lift (S O) O t2)))))).(\lambda (u: T).(\lambda (H3: (eq T +(THead (Flat Cast) u t0) (THead (Bind Void) u1 t1))).(let H4 \def (eq_ind T +(THead (Flat Cast) u t0) (\lambda (ee: T).(match ee with [(TSort _) +\Rightarrow False | (TLRef _) \Rightarrow False | (THead k _ _) \Rightarrow +(match k with [(Bind _) \Rightarrow False | (Flat _) \Rightarrow True])])) I +(THead (Bind Void) u1 t1) H3) in (False_ind (or (ex3_2 T T (\lambda (u2: +T).(\lambda (t3: T).(eq T t2 (THead (Bind Void) u2 t3)))) (\lambda (u2: +T).(\lambda (_: T).(pr0 u1 u2))) (\lambda (_: T).(\lambda (t3: T).(pr0 t1 +t3)))) (pr0 t1 (lift (S O) O t2))) H4)))))))) y x H0))) H)))).