X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fsoftware%2Fmatita%2Fcontribs%2FLAMBDA-TYPES%2FLambdaDelta-1%2Fty3%2Fpr3_props.ma;h=20d795000ffb91ead3cb52f2cb02da289405e162;hb=89519c7b52e06304a94019dd528925300380cdc0;hp=6cf0c095a55aa7652d81d89a689773899d2ff72b;hpb=831af787465e1bff886e22ee14b68c8f1bb0177c;p=helm.git diff --git a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma index 6cf0c095a..20d795000 100644 --- a/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma +++ b/helm/software/matita/contribs/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props.ma @@ -14,9 +14,7 @@ (* This file was automatically generated: do not edit *********************) -set "baseuri" "cic:/matita/LAMBDA-TYPES/LambdaDelta-1/ty3/pr3_props". - -include "ty3/pr3.ma". +include "LambdaDelta-1/ty3/pr3.ma". theorem ty3_cred_pr2: \forall (g: G).(\forall (c: C).(\forall (v1: T).(\forall (v2: T).((pr2 c v1 @@ -68,164 +66,165 @@ T).(ty3 g e t1 t2))))))))))) \def \lambda (g: G).(\lambda (c: C).(\lambda (t1: T).(\lambda (x: T).(\lambda (h: nat).(\lambda (d: nat).(\lambda (H: (ty3 g c (lift h d t1) x)).(insert_eq T -(lift h d t1) (\lambda (t: T).(ty3 g c t x)) (\forall (e: C).((drop h d c e) -\to (ex2 T (\lambda (t2: T).(pc3 c (lift h d t2) x)) (\lambda (t2: T).(ty3 g -e t1 t2))))) (\lambda (y: T).(\lambda (H0: (ty3 g c y x)).(unintro nat d -(\lambda (n: nat).((eq T y (lift h n t1)) \to (\forall (e: C).((drop h n c e) -\to (ex2 T (\lambda (t2: T).(pc3 c (lift h n t2) x)) (\lambda (t2: T).(ty3 g -e t1 t2))))))) (unintro T t1 (\lambda (t: T).(\forall (x0: nat).((eq T y -(lift h x0 t)) \to (\forall (e: C).((drop h x0 c e) \to (ex2 T (\lambda (t2: -T).(pc3 c (lift h x0 t2) x)) (\lambda (t2: T).(ty3 g e t t2)))))))) (ty3_ind -g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: T).(\forall (x0: T).(\forall -(x1: nat).((eq T t (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to -(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) t0)) (\lambda (t2: T).(ty3 g e -x0 t2))))))))))) (\lambda (c0: C).(\lambda (t2: T).(\lambda (t: T).(\lambda -(_: (ty3 g c0 t2 t)).(\lambda (_: ((\forall (x0: T).(\forall (x1: nat).((eq T -t2 (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to (ex2 T (\lambda -(t3: T).(pc3 c0 (lift h x1 t3) t)) (\lambda (t3: T).(ty3 g e x0 -t3)))))))))).(\lambda (u: T).(\lambda (t3: T).(\lambda (H3: (ty3 g c0 u -t3)).(\lambda (H4: ((\forall (x0: T).(\forall (x1: nat).((eq T u (lift h x1 -x0)) \to (\forall (e: C).((drop h x1 c0 e) \to (ex2 T (\lambda (t4: T).(pc3 -c0 (lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e x0 t4)))))))))).(\lambda -(H5: (pc3 c0 t3 t2)).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H6: (eq T -u (lift h x1 x0))).(\lambda (e: C).(\lambda (H7: (drop h x1 c0 e)).(let H8 -\def (eq_ind T u (\lambda (t0: T).(\forall (x2: T).(\forall (x3: nat).((eq T -t0 (lift h x3 x2)) \to (\forall (e0: C).((drop h x3 c0 e0) \to (ex2 T -(\lambda (t4: T).(pc3 c0 (lift h x3 t4) t3)) (\lambda (t4: T).(ty3 g e0 x2 -t4))))))))) H4 (lift h x1 x0) H6) in (let H9 \def (eq_ind T u (\lambda (t0: -T).(ty3 g c0 t0 t3)) H3 (lift h x1 x0) H6) in (let H10 \def (H8 x0 x1 -(refl_equal T (lift h x1 x0)) e H7) in (ex2_ind T (\lambda (t4: T).(pc3 c0 -(lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e x0 t4)) (ex2 T (\lambda (t4: -T).(pc3 c0 (lift h x1 t4) t2)) (\lambda (t4: T).(ty3 g e x0 t4))) (\lambda -(x2: T).(\lambda (H11: (pc3 c0 (lift h x1 x2) t3)).(\lambda (H12: (ty3 g e x0 -x2)).(ex_intro2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) t2)) (\lambda (t4: -T).(ty3 g e x0 t4)) x2 (pc3_t t3 c0 (lift h x1 x2) H11 t2 H5) H12)))) -H10))))))))))))))))))) (\lambda (c0: C).(\lambda (m: nat).(\lambda (x0: -T).(\lambda (x1: nat).(\lambda (H1: (eq T (TSort m) (lift h x1 x0))).(\lambda -(e: C).(\lambda (_: (drop h x1 c0 e)).(eq_ind_r T (TSort m) (\lambda (t: -T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (TSort (next g m)))) -(\lambda (t2: T).(ty3 g e t t2)))) (ex_intro2 T (\lambda (t2: T).(pc3 c0 -(lift h x1 t2) (TSort (next g m)))) (\lambda (t2: T).(ty3 g e (TSort m) t2)) -(TSort (next g m)) (eq_ind_r T (TSort (next g m)) (\lambda (t: T).(pc3 c0 t -(TSort (next g m)))) (pc3_refl c0 (TSort (next g m))) (lift h x1 (TSort (next -g m))) (lift_sort (next g m) h x1)) (ty3_sort g e m)) x0 (lift_gen_sort h x1 -m x0 H1))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda (d0: C).(\lambda -(u: T).(\lambda (H1: (getl n c0 (CHead d0 (Bind Abbr) u))).(\lambda (t: -T).(\lambda (H2: (ty3 g d0 u t)).(\lambda (H3: ((\forall (x0: T).(\forall -(x1: nat).((eq T u (lift h x1 x0)) \to (\forall (e: C).((drop h x1 d0 e) \to -(ex2 T (\lambda (t2: T).(pc3 d0 (lift h x1 t2) t)) (\lambda (t2: T).(ty3 g e -x0 t2)))))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H4: (eq T -(TLRef n) (lift h x1 x0))).(\lambda (e: C).(\lambda (H5: (drop h x1 c0 -e)).(let H_x \def (lift_gen_lref x0 x1 h n H4) in (let H6 \def H_x in (or_ind -(land (lt n x1) (eq T x0 (TLRef n))) (land (le (plus x1 h) n) (eq T x0 (TLRef -(minus n h)))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O -t))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H7: (land (lt n x1) (eq T -x0 (TLRef n)))).(and_ind (lt n x1) (eq T x0 (TLRef n)) (ex2 T (\lambda (t2: -T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e x0 -t2))) (\lambda (H8: (lt n x1)).(\lambda (H9: (eq T x0 (TLRef n))).(eq_ind_r T -(TLRef n) (\lambda (t0: T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) -(lift (S n) O t))) (\lambda (t2: T).(ty3 g e t0 t2)))) (let H10 \def (eq_ind -nat x1 (\lambda (n0: nat).(drop h n0 c0 e)) H5 (S (plus n (minus x1 (S n)))) -(lt_plus_minus n x1 H8)) in (ex3_2_ind T C (\lambda (v: T).(\lambda (_: -C).(eq T u (lift h (minus x1 (S n)) v)))) (\lambda (v: T).(\lambda (e0: -C).(getl n e (CHead e0 (Bind Abbr) v)))) (\lambda (_: T).(\lambda (e0: -C).(drop h (minus x1 (S n)) d0 e0))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h -x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e (TLRef n) t2))) (\lambda -(x2: T).(\lambda (x3: C).(\lambda (H11: (eq T u (lift h (minus x1 (S n)) -x2))).(\lambda (H12: (getl n e (CHead x3 (Bind Abbr) x2))).(\lambda (H13: -(drop h (minus x1 (S n)) d0 x3)).(let H14 \def (eq_ind T u (\lambda (t0: -T).(\forall (x4: T).(\forall (x5: nat).((eq T t0 (lift h x5 x4)) \to (\forall -(e0: C).((drop h x5 d0 e0) \to (ex2 T (\lambda (t2: T).(pc3 d0 (lift h x5 t2) -t)) (\lambda (t2: T).(ty3 g e0 x4 t2))))))))) H3 (lift h (minus x1 (S n)) x2) -H11) in (let H15 \def (eq_ind T u (\lambda (t0: T).(ty3 g d0 t0 t)) H2 (lift -h (minus x1 (S n)) x2) H11) in (let H16 \def (H14 x2 (minus x1 (S n)) -(refl_equal T (lift h (minus x1 (S n)) x2)) x3 H13) in (ex2_ind T (\lambda -(t2: T).(pc3 d0 (lift h (minus x1 (S n)) t2) t)) (\lambda (t2: T).(ty3 g x3 -x2 t2)) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) -(\lambda (t2: T).(ty3 g e (TLRef n) t2))) (\lambda (x4: T).(\lambda (H17: -(pc3 d0 (lift h (minus x1 (S n)) x4) t)).(\lambda (H18: (ty3 g x3 x2 -x4)).(eq_ind_r nat (plus (S n) (minus x1 (S n))) (\lambda (n0: nat).(ex2 T -(\lambda (t2: T).(pc3 c0 (lift h n0 t2) (lift (S n) O t))) (\lambda (t2: -T).(ty3 g e (TLRef n) t2)))) (ex_intro2 T (\lambda (t2: T).(pc3 c0 (lift h -(plus (S n) (minus x1 (S n))) t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g -e (TLRef n) t2)) (lift (S n) O x4) (eq_ind_r T (lift (S n) O (lift h (minus -x1 (S n)) x4)) (\lambda (t0: T).(pc3 c0 t0 (lift (S n) O t))) (pc3_lift c0 d0 -(S n) O (getl_drop Abbr c0 d0 u n H1) (lift h (minus x1 (S n)) x4) t H17) -(lift h (plus (S n) (minus x1 (S n))) (lift (S n) O x4)) (lift_d x4 h (S n) -(minus x1 (S n)) O (le_O_n (minus x1 (S n))))) (ty3_abbr g n e x3 x2 H12 x4 -H18)) x1 (le_plus_minus (S n) x1 H8))))) H16))))))))) (getl_drop_conf_lt Abbr -c0 d0 u n H1 e h (minus x1 (S n)) H10))) x0 H9))) H7)) (\lambda (H7: (land -(le (plus x1 h) n) (eq T x0 (TLRef (minus n h))))).(and_ind (le (plus x1 h) -n) (eq T x0 (TLRef (minus n h))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 -t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H8: (le -(plus x1 h) n)).(\lambda (H9: (eq T x0 (TLRef (minus n h)))).(eq_ind_r T -(TLRef (minus n h)) (\lambda (t0: T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h -x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e t0 t2)))) (ex_intro2 T +(lift h d t1) (\lambda (t: T).(ty3 g c t x)) (\lambda (_: T).(\forall (e: +C).((drop h d c e) \to (ex2 T (\lambda (t2: T).(pc3 c (lift h d t2) x)) +(\lambda (t2: T).(ty3 g e t1 t2)))))) (\lambda (y: T).(\lambda (H0: (ty3 g c +y x)).(unintro nat d (\lambda (n: nat).((eq T y (lift h n t1)) \to (\forall +(e: C).((drop h n c e) \to (ex2 T (\lambda (t2: T).(pc3 c (lift h n t2) x)) +(\lambda (t2: T).(ty3 g e t1 t2))))))) (unintro T t1 (\lambda (t: T).(\forall +(x0: nat).((eq T y (lift h x0 t)) \to (\forall (e: C).((drop h x0 c e) \to +(ex2 T (\lambda (t2: T).(pc3 c (lift h x0 t2) x)) (\lambda (t2: T).(ty3 g e t +t2)))))))) (ty3_ind g (\lambda (c0: C).(\lambda (t: T).(\lambda (t0: +T).(\forall (x0: T).(\forall (x1: nat).((eq T t (lift h x1 x0)) \to (\forall +(e: C).((drop h x1 c0 e) \to (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) +t0)) (\lambda (t2: T).(ty3 g e x0 t2))))))))))) (\lambda (c0: C).(\lambda +(t2: T).(\lambda (t: T).(\lambda (_: (ty3 g c0 t2 t)).(\lambda (_: ((\forall +(x0: T).(\forall (x1: nat).((eq T t2 (lift h x1 x0)) \to (\forall (e: +C).((drop h x1 c0 e) \to (ex2 T (\lambda (t3: T).(pc3 c0 (lift h x1 t3) t)) +(\lambda (t3: T).(ty3 g e x0 t3)))))))))).(\lambda (u: T).(\lambda (t3: +T).(\lambda (H3: (ty3 g c0 u t3)).(\lambda (H4: ((\forall (x0: T).(\forall +(x1: nat).((eq T u (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to +(ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e +x0 t4)))))))))).(\lambda (H5: (pc3 c0 t3 t2)).(\lambda (x0: T).(\lambda (x1: +nat).(\lambda (H6: (eq T u (lift h x1 x0))).(\lambda (e: C).(\lambda (H7: +(drop h x1 c0 e)).(let H8 \def (eq_ind T u (\lambda (t0: T).(\forall (x2: +T).(\forall (x3: nat).((eq T t0 (lift h x3 x2)) \to (\forall (e0: C).((drop h +x3 c0 e0) \to (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x3 t4) t3)) (\lambda +(t4: T).(ty3 g e0 x2 t4))))))))) H4 (lift h x1 x0) H6) in (let H9 \def +(eq_ind T u (\lambda (t0: T).(ty3 g c0 t0 t3)) H3 (lift h x1 x0) H6) in (let +H10 \def (H8 x0 x1 (refl_equal T (lift h x1 x0)) e H7) in (ex2_ind T (\lambda +(t4: T).(pc3 c0 (lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e x0 t4)) (ex2 T +(\lambda (t4: T).(pc3 c0 (lift h x1 t4) t2)) (\lambda (t4: T).(ty3 g e x0 +t4))) (\lambda (x2: T).(\lambda (H11: (pc3 c0 (lift h x1 x2) t3)).(\lambda +(H12: (ty3 g e x0 x2)).(ex_intro2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) +t2)) (\lambda (t4: T).(ty3 g e x0 t4)) x2 (pc3_t t3 c0 (lift h x1 x2) H11 t2 +H5) H12)))) H10))))))))))))))))))) (\lambda (c0: C).(\lambda (m: +nat).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H1: (eq T (TSort m) (lift +h x1 x0))).(\lambda (e: C).(\lambda (_: (drop h x1 c0 e)).(eq_ind_r T (TSort +m) (\lambda (t: T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (TSort +(next g m)))) (\lambda (t2: T).(ty3 g e t t2)))) (ex_intro2 T (\lambda (t2: +T).(pc3 c0 (lift h x1 t2) (TSort (next g m)))) (\lambda (t2: T).(ty3 g e +(TSort m) t2)) (TSort (next g m)) (eq_ind_r T (TSort (next g m)) (\lambda (t: +T).(pc3 c0 t (TSort (next g m)))) (pc3_refl c0 (TSort (next g m))) (lift h x1 +(TSort (next g m))) (lift_sort (next g m) h x1)) (ty3_sort g e m)) x0 +(lift_gen_sort h x1 m x0 H1))))))))) (\lambda (n: nat).(\lambda (c0: +C).(\lambda (d0: C).(\lambda (u: T).(\lambda (H1: (getl n c0 (CHead d0 (Bind +Abbr) u))).(\lambda (t: T).(\lambda (H2: (ty3 g d0 u t)).(\lambda (H3: +((\forall (x0: T).(\forall (x1: nat).((eq T u (lift h x1 x0)) \to (\forall +(e: C).((drop h x1 d0 e) \to (ex2 T (\lambda (t2: T).(pc3 d0 (lift h x1 t2) +t)) (\lambda (t2: T).(ty3 g e x0 t2)))))))))).(\lambda (x0: T).(\lambda (x1: +nat).(\lambda (H4: (eq T (TLRef n) (lift h x1 x0))).(\lambda (e: C).(\lambda +(H5: (drop h x1 c0 e)).(let H_x \def (lift_gen_lref x0 x1 h n H4) in (let H6 +\def H_x in (or_ind (land (lt n x1) (eq T x0 (TLRef n))) (land (le (plus x1 +h) n) (eq T x0 (TLRef (minus n h)))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h +x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H7: +(land (lt n x1) (eq T x0 (TLRef n)))).(land_ind (lt n x1) (eq T x0 (TLRef n)) +(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda +(t2: T).(ty3 g e x0 t2))) (\lambda (H8: (lt n x1)).(\lambda (H9: (eq T x0 +(TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ex2 T (\lambda (t2: +T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e t0 +t2)))) (let H10 \def (eq_ind nat x1 (\lambda (n0: nat).(drop h n0 c0 e)) H5 +(S (plus n (minus x1 (S n)))) (lt_plus_minus n x1 H8)) in (ex3_2_ind T C +(\lambda (v: T).(\lambda (_: C).(eq T u (lift h (minus x1 (S n)) v)))) +(\lambda (v: T).(\lambda (e0: C).(getl n e (CHead e0 (Bind Abbr) v)))) +(\lambda (_: T).(\lambda (e0: C).(drop h (minus x1 (S n)) d0 e0))) (ex2 T +(\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda (t2: +T).(ty3 g e (TLRef n) t2))) (\lambda (x2: T).(\lambda (x3: C).(\lambda (H11: +(eq T u (lift h (minus x1 (S n)) x2))).(\lambda (H12: (getl n e (CHead x3 +(Bind Abbr) x2))).(\lambda (H13: (drop h (minus x1 (S n)) d0 x3)).(let H14 +\def (eq_ind T u (\lambda (t0: T).(\forall (x4: T).(\forall (x5: nat).((eq T +t0 (lift h x5 x4)) \to (\forall (e0: C).((drop h x5 d0 e0) \to (ex2 T +(\lambda (t2: T).(pc3 d0 (lift h x5 t2) t)) (\lambda (t2: T).(ty3 g e0 x4 +t2))))))))) H3 (lift h (minus x1 (S n)) x2) H11) in (let H15 \def (eq_ind T u +(\lambda (t0: T).(ty3 g d0 t0 t)) H2 (lift h (minus x1 (S n)) x2) H11) in +(let H16 \def (H14 x2 (minus x1 (S n)) (refl_equal T (lift h (minus x1 (S n)) +x2)) x3 H13) in (ex2_ind T (\lambda (t2: T).(pc3 d0 (lift h (minus x1 (S n)) +t2) t)) (\lambda (t2: T).(ty3 g x3 x2 t2)) (ex2 T (\lambda (t2: T).(pc3 c0 +(lift h x1 t2) (lift (S n) O t))) (\lambda (t2: T).(ty3 g e (TLRef n) t2))) +(\lambda (x4: T).(\lambda (H17: (pc3 d0 (lift h (minus x1 (S n)) x4) +t)).(\lambda (H18: (ty3 g x3 x2 x4)).(eq_ind_r nat (plus (S n) (minus x1 (S +n))) (\lambda (n0: nat).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h n0 t2) (lift +(S n) O t))) (\lambda (t2: T).(ty3 g e (TLRef n) t2)))) (ex_intro2 T (\lambda +(t2: T).(pc3 c0 (lift h (plus (S n) (minus x1 (S n))) t2) (lift (S n) O t))) +(\lambda (t2: T).(ty3 g e (TLRef n) t2)) (lift (S n) O x4) (eq_ind_r T (lift +(S n) O (lift h (minus x1 (S n)) x4)) (\lambda (t0: T).(pc3 c0 t0 (lift (S n) +O t))) (pc3_lift c0 d0 (S n) O (getl_drop Abbr c0 d0 u n H1) (lift h (minus +x1 (S n)) x4) t H17) (lift h (plus (S n) (minus x1 (S n))) (lift (S n) O x4)) +(lift_d x4 h (S n) (minus x1 (S n)) O (le_O_n (minus x1 (S n))))) (ty3_abbr g +n e x3 x2 H12 x4 H18)) x1 (le_plus_minus (S n) x1 H8))))) H16))))))))) +(getl_drop_conf_lt Abbr c0 d0 u n H1 e h (minus x1 (S n)) H10))) x0 H9))) +H7)) (\lambda (H7: (land (le (plus x1 h) n) (eq T x0 (TLRef (minus n +h))))).(land_ind (le (plus x1 h) n) (eq T x0 (TLRef (minus n h))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda (t2: -T).(ty3 g e (TLRef (minus n h)) t2)) (lift (S (minus n h)) O t) (eq_ind_r T -(lift (plus h (S (minus n h))) O t) (\lambda (t0: T).(pc3 c0 t0 (lift (S n) O -t))) (eq_ind nat (S (plus h (minus n h))) (\lambda (n0: nat).(pc3 c0 (lift n0 -O t) (lift (S n) O t))) (eq_ind nat n (\lambda (n0: nat).(pc3 c0 (lift (S n0) -O t) (lift (S n) O t))) (pc3_refl c0 (lift (S n) O t)) (plus h (minus n h)) -(le_plus_minus h n (le_trans_plus_r x1 h n H8))) (plus h (S (minus n h))) -(plus_n_Sm h (minus n h))) (lift h x1 (lift (S (minus n h)) O t)) (lift_free -t (S (minus n h)) h O x1 (le_trans x1 (S (minus n h)) (plus O (S (minus n -h))) (le_S_minus x1 h n H8) (le_n (plus O (S (minus n h))))) (le_O_n x1))) -(ty3_abbr g (minus n h) e d0 u (getl_drop_conf_ge n (CHead d0 (Bind Abbr) u) -c0 H1 e h x1 H5 H8) t H2)) x0 H9))) H7)) H6)))))))))))))))) (\lambda (n: -nat).(\lambda (c0: C).(\lambda (d0: C).(\lambda (u: T).(\lambda (H1: (getl n -c0 (CHead d0 (Bind Abst) u))).(\lambda (t: T).(\lambda (H2: (ty3 g d0 u -t)).(\lambda (H3: ((\forall (x0: T).(\forall (x1: nat).((eq T u (lift h x1 -x0)) \to (\forall (e: C).((drop h x1 d0 e) \to (ex2 T (\lambda (t2: T).(pc3 -d0 (lift h x1 t2) t)) (\lambda (t2: T).(ty3 g e x0 t2)))))))))).(\lambda (x0: -T).(\lambda (x1: nat).(\lambda (H4: (eq T (TLRef n) (lift h x1 x0))).(\lambda -(e: C).(\lambda (H5: (drop h x1 c0 e)).(let H_x \def (lift_gen_lref x0 x1 h n -H4) in (let H6 \def H_x in (or_ind (land (lt n x1) (eq T x0 (TLRef n))) (land -(le (plus x1 h) n) (eq T x0 (TLRef (minus n h)))) (ex2 T (\lambda (t2: -T).(pc3 c0 (lift h x1 t2) (lift (S n) O u))) (\lambda (t2: T).(ty3 g e x0 -t2))) (\lambda (H7: (land (lt n x1) (eq T x0 (TLRef n)))).(and_ind (lt n x1) -(eq T x0 (TLRef n)) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S -n) O u))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H8: (lt n -x1)).(\lambda (H9: (eq T x0 (TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0: -T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O u))) (\lambda -(t2: T).(ty3 g e t0 t2)))) (let H10 \def (eq_ind nat x1 (\lambda (n0: -nat).(drop h n0 c0 e)) H5 (S (plus n (minus x1 (S n)))) (lt_plus_minus n x1 -H8)) in (ex3_2_ind T C (\lambda (v: T).(\lambda (_: C).(eq T u (lift h (minus -x1 (S n)) v)))) (\lambda (v: T).(\lambda (e0: C).(getl n e (CHead e0 (Bind -Abst) v)))) (\lambda (_: T).(\lambda (e0: C).(drop h (minus x1 (S n)) d0 -e0))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O u))) -(\lambda (t2: T).(ty3 g e (TLRef n) t2))) (\lambda (x2: T).(\lambda (x3: -C).(\lambda (H11: (eq T u (lift h (minus x1 (S n)) x2))).(\lambda (H12: (getl -n e (CHead x3 (Bind Abst) x2))).(\lambda (H13: (drop h (minus x1 (S n)) d0 -x3)).(let H14 \def (eq_ind T u (\lambda (t0: T).(\forall (x4: T).(\forall -(x5: nat).((eq T t0 (lift h x5 x4)) \to (\forall (e0: C).((drop h x5 d0 e0) -\to (ex2 T (\lambda (t2: T).(pc3 d0 (lift h x5 t2) t)) (\lambda (t2: T).(ty3 -g e0 x4 t2))))))))) H3 (lift h (minus x1 (S n)) x2) H11) in (let H15 \def -(eq_ind T u (\lambda (t0: T).(ty3 g d0 t0 t)) H2 (lift h (minus x1 (S n)) x2) -H11) in (eq_ind_r T (lift h (minus x1 (S n)) x2) (\lambda (t0: T).(ex2 T -(\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t0))) (\lambda (t2: -T).(ty3 g e (TLRef n) t2)))) (let H16 \def (H14 x2 (minus x1 (S n)) -(refl_equal T (lift h (minus x1 (S n)) x2)) x3 H13) in (ex2_ind T (\lambda -(t2: T).(pc3 d0 (lift h (minus x1 (S n)) t2) t)) (\lambda (t2: T).(ty3 g x3 -x2 t2)) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O (lift h -(minus x1 (S n)) x2)))) (\lambda (t2: T).(ty3 g e (TLRef n) t2))) (\lambda -(x4: T).(\lambda (_: (pc3 d0 (lift h (minus x1 (S n)) x4) t)).(\lambda (H18: -(ty3 g x3 x2 x4)).(eq_ind_r nat (plus (S n) (minus x1 (S n))) (\lambda (n0: -nat).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h n0 t2) (lift (S n) O (lift h -(minus n0 (S n)) x2)))) (\lambda (t2: T).(ty3 g e (TLRef n) t2)))) (ex_intro2 -T (\lambda (t2: T).(pc3 c0 (lift h (plus (S n) (minus x1 (S n))) t2) (lift (S -n) O (lift h (minus (plus (S n) (minus x1 (S n))) (S n)) x2)))) (\lambda (t2: -T).(ty3 g e (TLRef n) t2)) (lift (S n) O x2) (eq_ind_r T (lift (S n) O (lift -h (minus x1 (S n)) x2)) (\lambda (t0: T).(pc3 c0 t0 (lift (S n) O (lift h -(minus (plus (S n) (minus x1 (S n))) (S n)) x2)))) (eq_ind nat x1 (\lambda -(n0: nat).(pc3 c0 (lift (S n) O (lift h (minus x1 (S n)) x2)) (lift (S n) O -(lift h (minus n0 (S n)) x2)))) (pc3_refl c0 (lift (S n) O (lift h (minus x1 -(S n)) x2))) (plus (S n) (minus x1 (S n))) (le_plus_minus (S n) x1 H8)) (lift -h (plus (S n) (minus x1 (S n))) (lift (S n) O x2)) (lift_d x2 h (S n) (minus -x1 (S n)) O (le_O_n (minus x1 (S n))))) (ty3_abst g n e x3 x2 H12 x4 H18)) x1 +T).(ty3 g e x0 t2))) (\lambda (H8: (le (plus x1 h) n)).(\lambda (H9: (eq T x0 +(TLRef (minus n h)))).(eq_ind_r T (TLRef (minus n h)) (\lambda (t0: T).(ex2 T +(\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t))) (\lambda (t2: +T).(ty3 g e t0 t2)))) (ex_intro2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) +(lift (S n) O t))) (\lambda (t2: T).(ty3 g e (TLRef (minus n h)) t2)) (lift +(S (minus n h)) O t) (eq_ind_r T (lift (plus h (S (minus n h))) O t) (\lambda +(t0: T).(pc3 c0 t0 (lift (S n) O t))) (eq_ind nat (S (plus h (minus n h))) +(\lambda (n0: nat).(pc3 c0 (lift n0 O t) (lift (S n) O t))) (eq_ind nat n +(\lambda (n0: nat).(pc3 c0 (lift (S n0) O t) (lift (S n) O t))) (pc3_refl c0 +(lift (S n) O t)) (plus h (minus n h)) (le_plus_minus h n (le_trans h (plus +x1 h) n (le_plus_r x1 h) H8))) (plus h (S (minus n h))) (plus_n_Sm h (minus n +h))) (lift h x1 (lift (S (minus n h)) O t)) (lift_free t (S (minus n h)) h O +x1 (le_trans x1 (S (minus n h)) (plus O (S (minus n h))) (le_S_minus x1 h n +H8) (le_n (plus O (S (minus n h))))) (le_O_n x1))) (ty3_abbr g (minus n h) e +d0 u (getl_drop_conf_ge n (CHead d0 (Bind Abbr) u) c0 H1 e h x1 H5 H8) t H2)) +x0 H9))) H7)) H6)))))))))))))))) (\lambda (n: nat).(\lambda (c0: C).(\lambda +(d0: C).(\lambda (u: T).(\lambda (H1: (getl n c0 (CHead d0 (Bind Abst) +u))).(\lambda (t: T).(\lambda (H2: (ty3 g d0 u t)).(\lambda (H3: ((\forall +(x0: T).(\forall (x1: nat).((eq T u (lift h x1 x0)) \to (\forall (e: +C).((drop h x1 d0 e) \to (ex2 T (\lambda (t2: T).(pc3 d0 (lift h x1 t2) t)) +(\lambda (t2: T).(ty3 g e x0 t2)))))))))).(\lambda (x0: T).(\lambda (x1: +nat).(\lambda (H4: (eq T (TLRef n) (lift h x1 x0))).(\lambda (e: C).(\lambda +(H5: (drop h x1 c0 e)).(let H_x \def (lift_gen_lref x0 x1 h n H4) in (let H6 +\def H_x in (or_ind (land (lt n x1) (eq T x0 (TLRef n))) (land (le (plus x1 +h) n) (eq T x0 (TLRef (minus n h)))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h +x1 t2) (lift (S n) O u))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H7: +(land (lt n x1) (eq T x0 (TLRef n)))).(land_ind (lt n x1) (eq T x0 (TLRef n)) +(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O u))) (\lambda +(t2: T).(ty3 g e x0 t2))) (\lambda (H8: (lt n x1)).(\lambda (H9: (eq T x0 +(TLRef n))).(eq_ind_r T (TLRef n) (\lambda (t0: T).(ex2 T (\lambda (t2: +T).(pc3 c0 (lift h x1 t2) (lift (S n) O u))) (\lambda (t2: T).(ty3 g e t0 +t2)))) (let H10 \def (eq_ind nat x1 (\lambda (n0: nat).(drop h n0 c0 e)) H5 +(S (plus n (minus x1 (S n)))) (lt_plus_minus n x1 H8)) in (ex3_2_ind T C +(\lambda (v: T).(\lambda (_: C).(eq T u (lift h (minus x1 (S n)) v)))) +(\lambda (v: T).(\lambda (e0: C).(getl n e (CHead e0 (Bind Abst) v)))) +(\lambda (_: T).(\lambda (e0: C).(drop h (minus x1 (S n)) d0 e0))) (ex2 T +(\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O u))) (\lambda (t2: +T).(ty3 g e (TLRef n) t2))) (\lambda (x2: T).(\lambda (x3: C).(\lambda (H11: +(eq T u (lift h (minus x1 (S n)) x2))).(\lambda (H12: (getl n e (CHead x3 +(Bind Abst) x2))).(\lambda (H13: (drop h (minus x1 (S n)) d0 x3)).(let H14 +\def (eq_ind T u (\lambda (t0: T).(\forall (x4: T).(\forall (x5: nat).((eq T +t0 (lift h x5 x4)) \to (\forall (e0: C).((drop h x5 d0 e0) \to (ex2 T +(\lambda (t2: T).(pc3 d0 (lift h x5 t2) t)) (\lambda (t2: T).(ty3 g e0 x4 +t2))))))))) H3 (lift h (minus x1 (S n)) x2) H11) in (let H15 \def (eq_ind T u +(\lambda (t0: T).(ty3 g d0 t0 t)) H2 (lift h (minus x1 (S n)) x2) H11) in +(eq_ind_r T (lift h (minus x1 (S n)) x2) (\lambda (t0: T).(ex2 T (\lambda +(t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O t0))) (\lambda (t2: T).(ty3 g e +(TLRef n) t2)))) (let H16 \def (H14 x2 (minus x1 (S n)) (refl_equal T (lift h +(minus x1 (S n)) x2)) x3 H13) in (ex2_ind T (\lambda (t2: T).(pc3 d0 (lift h +(minus x1 (S n)) t2) t)) (\lambda (t2: T).(ty3 g x3 x2 t2)) (ex2 T (\lambda +(t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O (lift h (minus x1 (S n)) x2)))) +(\lambda (t2: T).(ty3 g e (TLRef n) t2))) (\lambda (x4: T).(\lambda (_: (pc3 +d0 (lift h (minus x1 (S n)) x4) t)).(\lambda (H18: (ty3 g x3 x2 +x4)).(eq_ind_r nat (plus (S n) (minus x1 (S n))) (\lambda (n0: nat).(ex2 T +(\lambda (t2: T).(pc3 c0 (lift h n0 t2) (lift (S n) O (lift h (minus n0 (S +n)) x2)))) (\lambda (t2: T).(ty3 g e (TLRef n) t2)))) (ex_intro2 T (\lambda +(t2: T).(pc3 c0 (lift h (plus (S n) (minus x1 (S n))) t2) (lift (S n) O (lift +h (minus (plus (S n) (minus x1 (S n))) (S n)) x2)))) (\lambda (t2: T).(ty3 g +e (TLRef n) t2)) (lift (S n) O x2) (eq_ind_r T (lift (S n) O (lift h (minus +x1 (S n)) x2)) (\lambda (t0: T).(pc3 c0 t0 (lift (S n) O (lift h (minus (plus +(S n) (minus x1 (S n))) (S n)) x2)))) (eq_ind nat x1 (\lambda (n0: nat).(pc3 +c0 (lift (S n) O (lift h (minus x1 (S n)) x2)) (lift (S n) O (lift h (minus +n0 (S n)) x2)))) (pc3_refl c0 (lift (S n) O (lift h (minus x1 (S n)) x2))) +(plus (S n) (minus x1 (S n))) (le_plus_minus (S n) x1 H8)) (lift h (plus (S +n) (minus x1 (S n))) (lift (S n) O x2)) (lift_d x2 h (S n) (minus x1 (S n)) O +(le_O_n (minus x1 (S n))))) (ty3_abst g n e x3 x2 H12 x4 H18)) x1 (le_plus_minus (S n) x1 H8))))) H16)) u H11)))))))) (getl_drop_conf_lt Abst c0 d0 u n H1 e h (minus x1 (S n)) H10))) x0 H9))) H7)) (\lambda (H7: (land -(le (plus x1 h) n) (eq T x0 (TLRef (minus n h))))).(and_ind (le (plus x1 h) +(le (plus x1 h) n) (eq T x0 (TLRef (minus n h))))).(land_ind (le (plus x1 h) n) (eq T x0 (TLRef (minus n h))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (lift (S n) O u))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (H8: (le (plus x1 h) n)).(\lambda (H9: (eq T x0 (TLRef (minus n h)))).(eq_ind_r T @@ -237,150 +236,138 @@ T).(ty3 g e (TLRef (minus n h)) t2)) (lift (S (minus n h)) O u) (eq_ind_r T u))) (eq_ind nat (S (plus h (minus n h))) (\lambda (n0: nat).(pc3 c0 (lift n0 O u) (lift (S n) O u))) (eq_ind nat n (\lambda (n0: nat).(pc3 c0 (lift (S n0) O u) (lift (S n) O u))) (pc3_refl c0 (lift (S n) O u)) (plus h (minus n h)) -(le_plus_minus h n (le_trans_plus_r x1 h n H8))) (plus h (S (minus n h))) -(plus_n_Sm h (minus n h))) (lift h x1 (lift (S (minus n h)) O u)) (lift_free -u (S (minus n h)) h O x1 (le_trans x1 (S (minus n h)) (plus O (S (minus n -h))) (le_S_minus x1 h n H8) (le_n (plus O (S (minus n h))))) (le_O_n x1))) -(ty3_abst g (minus n h) e d0 u (getl_drop_conf_ge n (CHead d0 (Bind Abst) u) -c0 H1 e h x1 H5 H8) t H2)) x0 H9))) H7)) H6)))))))))))))))) (\lambda (c0: -C).(\lambda (u: T).(\lambda (t: T).(\lambda (H1: (ty3 g c0 u t)).(\lambda -(H2: ((\forall (x0: T).(\forall (x1: nat).((eq T u (lift h x1 x0)) \to -(\forall (e: C).((drop h x1 c0 e) \to (ex2 T (\lambda (t2: T).(pc3 c0 (lift h -x1 t2) t)) (\lambda (t2: T).(ty3 g e x0 t2)))))))))).(\lambda (b: B).(\lambda -(t2: T).(\lambda (t3: T).(\lambda (H3: (ty3 g (CHead c0 (Bind b) u) t2 -t3)).(\lambda (H4: ((\forall (x0: T).(\forall (x1: nat).((eq T t2 (lift h x1 -x0)) \to (\forall (e: C).((drop h x1 (CHead c0 (Bind b) u) e) \to (ex2 T +(le_plus_minus h n (le_trans h (plus x1 h) n (le_plus_r x1 h) H8))) (plus h +(S (minus n h))) (plus_n_Sm h (minus n h))) (lift h x1 (lift (S (minus n h)) +O u)) (lift_free u (S (minus n h)) h O x1 (le_trans x1 (S (minus n h)) (plus +O (S (minus n h))) (le_S_minus x1 h n H8) (le_n (plus O (S (minus n h))))) +(le_O_n x1))) (ty3_abst g (minus n h) e d0 u (getl_drop_conf_ge n (CHead d0 +(Bind Abst) u) c0 H1 e h x1 H5 H8) t H2)) x0 H9))) H7)) H6)))))))))))))))) +(\lambda (c0: C).(\lambda (u: T).(\lambda (t: T).(\lambda (H1: (ty3 g c0 u +t)).(\lambda (H2: ((\forall (x0: T).(\forall (x1: nat).((eq T u (lift h x1 +x0)) \to (\forall (e: C).((drop h x1 c0 e) \to (ex2 T (\lambda (t2: T).(pc3 +c0 (lift h x1 t2) t)) (\lambda (t2: T).(ty3 g e x0 t2)))))))))).(\lambda (b: +B).(\lambda (t2: T).(\lambda (t3: T).(\lambda (H3: (ty3 g (CHead c0 (Bind b) +u) t2 t3)).(\lambda (H4: ((\forall (x0: T).(\forall (x1: nat).((eq T t2 (lift +h x1 x0)) \to (\forall (e: C).((drop h x1 (CHead c0 (Bind b) u) e) \to (ex2 T (\lambda (t4: T).(pc3 (CHead c0 (Bind b) u) (lift h x1 t4) t3)) (\lambda (t4: -T).(ty3 g e x0 t4)))))))))).(\lambda (t0: T).(\lambda (H5: (ty3 g (CHead c0 -(Bind b) u) t3 t0)).(\lambda (H6: ((\forall (x0: T).(\forall (x1: nat).((eq T -t3 (lift h x1 x0)) \to (\forall (e: C).((drop h x1 (CHead c0 (Bind b) u) e) -\to (ex2 T (\lambda (t4: T).(pc3 (CHead c0 (Bind b) u) (lift h x1 t4) t0)) -(\lambda (t4: T).(ty3 g e x0 t4)))))))))).(\lambda (x0: T).(\lambda (x1: -nat).(\lambda (H7: (eq T (THead (Bind b) u t2) (lift h x1 x0))).(\lambda (e: -C).(\lambda (H8: (drop h x1 c0 e)).(ex3_2_ind T T (\lambda (y0: T).(\lambda -(z: T).(eq T x0 (THead (Bind b) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq -T u (lift h x1 y0)))) (\lambda (_: T).(\lambda (z: T).(eq T t2 (lift h (S x1) -z)))) (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Bind b) u t3))) -(\lambda (t4: T).(ty3 g e x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda -(H9: (eq T x0 (THead (Bind b) x2 x3))).(\lambda (H10: (eq T u (lift h x1 -x2))).(\lambda (H11: (eq T t2 (lift h (S x1) x3))).(eq_ind_r T (THead (Bind -b) x2 x3) (\lambda (t4: T).(ex2 T (\lambda (t5: T).(pc3 c0 (lift h x1 t5) -(THead (Bind b) u t3))) (\lambda (t5: T).(ty3 g e t4 t5)))) (let H12 \def -(eq_ind T t2 (\lambda (t4: T).(\forall (x4: T).(\forall (x5: nat).((eq T t4 -(lift h x5 x4)) \to (\forall (e0: C).((drop h x5 (CHead c0 (Bind b) u) e0) -\to (ex2 T (\lambda (t5: T).(pc3 (CHead c0 (Bind b) u) (lift h x5 t5) t3)) -(\lambda (t5: T).(ty3 g e0 x4 t5))))))))) H4 (lift h (S x1) x3) H11) in (let -H13 \def (eq_ind T t2 (\lambda (t4: T).(ty3 g (CHead c0 (Bind b) u) t4 t3)) -H3 (lift h (S x1) x3) H11) in (let H14 \def (eq_ind T u (\lambda (t4: T).(ty3 -g (CHead c0 (Bind b) t4) (lift h (S x1) x3) t3)) H13 (lift h x1 x2) H10) in -(let H15 \def (eq_ind T u (\lambda (t4: T).(\forall (x4: T).(\forall (x5: -nat).((eq T (lift h (S x1) x3) (lift h x5 x4)) \to (\forall (e0: C).((drop h -x5 (CHead c0 (Bind b) t4) e0) \to (ex2 T (\lambda (t5: T).(pc3 (CHead c0 -(Bind b) t4) (lift h x5 t5) t3)) (\lambda (t5: T).(ty3 g e0 x4 t5))))))))) -H12 (lift h x1 x2) H10) in (let H16 \def (eq_ind T u (\lambda (t4: -T).(\forall (x4: T).(\forall (x5: nat).((eq T t3 (lift h x5 x4)) \to (\forall -(e0: C).((drop h x5 (CHead c0 (Bind b) t4) e0) \to (ex2 T (\lambda (t5: -T).(pc3 (CHead c0 (Bind b) t4) (lift h x5 t5) t0)) (\lambda (t5: T).(ty3 g e0 -x4 t5))))))))) H6 (lift h x1 x2) H10) in (let H17 \def (eq_ind T u (\lambda -(t4: T).(ty3 g (CHead c0 (Bind b) t4) t3 t0)) H5 (lift h x1 x2) H10) in (let -H18 \def (eq_ind T u (\lambda (t4: T).(\forall (x4: T).(\forall (x5: -nat).((eq T t4 (lift h x5 x4)) \to (\forall (e0: C).((drop h x5 c0 e0) \to -(ex2 T (\lambda (t5: T).(pc3 c0 (lift h x5 t5) t)) (\lambda (t5: T).(ty3 g e0 -x4 t5))))))))) H2 (lift h x1 x2) H10) in (let H19 \def (eq_ind T u (\lambda -(t4: T).(ty3 g c0 t4 t)) H1 (lift h x1 x2) H10) in (eq_ind_r T (lift h x1 x2) -(\lambda (t4: T).(ex2 T (\lambda (t5: T).(pc3 c0 (lift h x1 t5) (THead (Bind -b) t4 t3))) (\lambda (t5: T).(ty3 g e (THead (Bind b) x2 x3) t5)))) (let H20 -\def (H18 x2 x1 (refl_equal T (lift h x1 x2)) e H8) in (ex2_ind T (\lambda +T).(ty3 g e x0 t4)))))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H5: +(eq T (THead (Bind b) u t2) (lift h x1 x0))).(\lambda (e: C).(\lambda (H6: +(drop h x1 c0 e)).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x0 +(THead (Bind b) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T u (lift h x1 +y0)))) (\lambda (_: T).(\lambda (z: T).(eq T t2 (lift h (S x1) z)))) (ex2 T +(\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Bind b) u t3))) (\lambda (t4: +T).(ty3 g e x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7: (eq T x0 +(THead (Bind b) x2 x3))).(\lambda (H8: (eq T u (lift h x1 x2))).(\lambda (H9: +(eq T t2 (lift h (S x1) x3))).(eq_ind_r T (THead (Bind b) x2 x3) (\lambda +(t0: T).(ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Bind b) u +t3))) (\lambda (t4: T).(ty3 g e t0 t4)))) (let H10 \def (eq_ind T t2 (\lambda +(t0: T).(\forall (x4: T).(\forall (x5: nat).((eq T t0 (lift h x5 x4)) \to +(\forall (e0: C).((drop h x5 (CHead c0 (Bind b) u) e0) \to (ex2 T (\lambda +(t4: T).(pc3 (CHead c0 (Bind b) u) (lift h x5 t4) t3)) (\lambda (t4: T).(ty3 +g e0 x4 t4))))))))) H4 (lift h (S x1) x3) H9) in (let H11 \def (eq_ind T t2 +(\lambda (t0: T).(ty3 g (CHead c0 (Bind b) u) t0 t3)) H3 (lift h (S x1) x3) +H9) in (let H12 \def (eq_ind T u (\lambda (t0: T).(ty3 g (CHead c0 (Bind b) +t0) (lift h (S x1) x3) t3)) H11 (lift h x1 x2) H8) in (let H13 \def (eq_ind T +u (\lambda (t0: T).(\forall (x4: T).(\forall (x5: nat).((eq T (lift h (S x1) +x3) (lift h x5 x4)) \to (\forall (e0: C).((drop h x5 (CHead c0 (Bind b) t0) +e0) \to (ex2 T (\lambda (t4: T).(pc3 (CHead c0 (Bind b) t0) (lift h x5 t4) +t3)) (\lambda (t4: T).(ty3 g e0 x4 t4))))))))) H10 (lift h x1 x2) H8) in (let +H14 \def (eq_ind T u (\lambda (t0: T).(\forall (x4: T).(\forall (x5: +nat).((eq T t0 (lift h x5 x4)) \to (\forall (e0: C).((drop h x5 c0 e0) \to +(ex2 T (\lambda (t4: T).(pc3 c0 (lift h x5 t4) t)) (\lambda (t4: T).(ty3 g e0 +x4 t4))))))))) H2 (lift h x1 x2) H8) in (let H15 \def (eq_ind T u (\lambda +(t0: T).(ty3 g c0 t0 t)) H1 (lift h x1 x2) H8) in (eq_ind_r T (lift h x1 x2) +(\lambda (t0: T).(ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Bind +b) t0 t3))) (\lambda (t4: T).(ty3 g e (THead (Bind b) x2 x3) t4)))) (let H16 +\def (H14 x2 x1 (refl_equal T (lift h x1 x2)) e H6) in (ex2_ind T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) t)) (\lambda (t4: T).(ty3 g e x2 t4)) (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3))) (\lambda (t4: T).(ty3 g e (THead (Bind b) x2 x3) t4))) (\lambda (x4: -T).(\lambda (_: (pc3 c0 (lift h x1 x4) t)).(\lambda (H22: (ty3 g e x2 -x4)).(let H23 \def (H15 x3 (S x1) (refl_equal T (lift h (S x1) x3)) (CHead e -(Bind b) x2) (drop_skip_bind h x1 c0 e H8 b x2)) in (ex2_ind T (\lambda (t4: +T).(\lambda (_: (pc3 c0 (lift h x1 x4) t)).(\lambda (H18: (ty3 g e x2 +x4)).(let H19 \def (H13 x3 (S x1) (refl_equal T (lift h (S x1) x3)) (CHead e +(Bind b) x2) (drop_skip_bind h x1 c0 e H6 b x2)) in (ex2_ind T (\lambda (t4: T).(pc3 (CHead c0 (Bind b) (lift h x1 x2)) (lift h (S x1) t4) t3)) (\lambda (t4: T).(ty3 g (CHead e (Bind b) x2) x3 t4)) (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3))) (\lambda (t4: T).(ty3 g e -(THead (Bind b) x2 x3) t4))) (\lambda (x5: T).(\lambda (H24: (pc3 (CHead c0 -(Bind b) (lift h x1 x2)) (lift h (S x1) x5) t3)).(\lambda (H25: (ty3 g (CHead -e (Bind b) x2) x3 x5)).(ex_ind T (\lambda (t4: T).(ty3 g (CHead e (Bind b) -x2) x5 t4)) (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Bind b) +(THead (Bind b) x2 x3) t4))) (\lambda (x5: T).(\lambda (H20: (pc3 (CHead c0 +(Bind b) (lift h x1 x2)) (lift h (S x1) x5) t3)).(\lambda (H21: (ty3 g (CHead +e (Bind b) x2) x3 x5)).(ex_ind T (\lambda (t0: T).(ty3 g (CHead e (Bind b) +x2) x5 t0)) (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) t3))) (\lambda (t4: T).(ty3 g e (THead (Bind b) x2 x3) t4))) -(\lambda (x6: T).(\lambda (H26: (ty3 g (CHead e (Bind b) x2) x5 -x6)).(ex_intro2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Bind b) -(lift h x1 x2) t3))) (\lambda (t4: T).(ty3 g e (THead (Bind b) x2 x3) t4)) -(THead (Bind b) x2 x5) (eq_ind_r T (THead (Bind b) (lift h x1 x2) (lift h (S -x1) x5)) (\lambda (t4: T).(pc3 c0 t4 (THead (Bind b) (lift h x1 x2) t3))) -(pc3_head_2 c0 (lift h x1 x2) (lift h (S x1) x5) t3 (Bind b) H24) (lift h x1 -(THead (Bind b) x2 x5)) (lift_bind b x2 x5 h x1)) (ty3_bind g e x2 x4 H22 b -x3 x5 H25 x6 H26)))) (ty3_correct g (CHead e (Bind b) x2) x3 x5 H25))))) -H23))))) H20)) u H10))))))))) x0 H9)))))) (lift_gen_bind b u t2 x0 h x1 -H7)))))))))))))))))))) (\lambda (c0: C).(\lambda (w: T).(\lambda (u: -T).(\lambda (H1: (ty3 g c0 w u)).(\lambda (H2: ((\forall (x0: T).(\forall -(x1: nat).((eq T w (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to -(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) u)) (\lambda (t2: T).(ty3 g e -x0 t2)))))))))).(\lambda (v: T).(\lambda (t: T).(\lambda (H3: (ty3 g c0 v -(THead (Bind Abst) u t))).(\lambda (H4: ((\forall (x0: T).(\forall (x1: -nat).((eq T v (lift h x1 x0)) \to (\forall (e: C).((drop h x1 c0 e) \to (ex2 -T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Bind Abst) u t))) (\lambda -(t2: T).(ty3 g e x0 t2)))))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda -(H5: (eq T (THead (Flat Appl) w v) (lift h x1 x0))).(\lambda (e: C).(\lambda -(H6: (drop h x1 c0 e)).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T -x0 (THead (Flat Appl) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T w (lift -h x1 y0)))) (\lambda (_: T).(\lambda (z: T).(eq T v (lift h x1 z)))) (ex2 T -(\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) w (THead (Bind -Abst) u t)))) (\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (x2: T).(\lambda -(x3: T).(\lambda (H7: (eq T x0 (THead (Flat Appl) x2 x3))).(\lambda (H8: (eq -T w (lift h x1 x2))).(\lambda (H9: (eq T v (lift h x1 x3))).(eq_ind_r T -(THead (Flat Appl) x2 x3) (\lambda (t0: T).(ex2 T (\lambda (t2: T).(pc3 c0 -(lift h x1 t2) (THead (Flat Appl) w (THead (Bind Abst) u t)))) (\lambda (t2: -T).(ty3 g e t0 t2)))) (let H10 \def (eq_ind T v (\lambda (t0: T).(\forall +(\lambda (x6: T).(\lambda (_: (ty3 g (CHead e (Bind b) x2) x5 x6)).(ex_intro2 +T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Bind b) (lift h x1 x2) +t3))) (\lambda (t4: T).(ty3 g e (THead (Bind b) x2 x3) t4)) (THead (Bind b) +x2 x5) (eq_ind_r T (THead (Bind b) (lift h x1 x2) (lift h (S x1) x5)) +(\lambda (t0: T).(pc3 c0 t0 (THead (Bind b) (lift h x1 x2) t3))) (pc3_head_2 +c0 (lift h x1 x2) (lift h (S x1) x5) t3 (Bind b) H20) (lift h x1 (THead (Bind +b) x2 x5)) (lift_bind b x2 x5 h x1)) (ty3_bind g e x2 x4 H18 b x3 x5 H21)))) +(ty3_correct g (CHead e (Bind b) x2) x3 x5 H21))))) H19))))) H16)) u +H8))))))) x0 H7)))))) (lift_gen_bind b u t2 x0 h x1 H5))))))))))))))))) +(\lambda (c0: C).(\lambda (w: T).(\lambda (u: T).(\lambda (H1: (ty3 g c0 w +u)).(\lambda (H2: ((\forall (x0: T).(\forall (x1: nat).((eq T w (lift h x1 +x0)) \to (\forall (e: C).((drop h x1 c0 e) \to (ex2 T (\lambda (t2: T).(pc3 +c0 (lift h x1 t2) u)) (\lambda (t2: T).(ty3 g e x0 t2)))))))))).(\lambda (v: +T).(\lambda (t: T).(\lambda (H3: (ty3 g c0 v (THead (Bind Abst) u +t))).(\lambda (H4: ((\forall (x0: T).(\forall (x1: nat).((eq T v (lift h x1 +x0)) \to (\forall (e: C).((drop h x1 c0 e) \to (ex2 T (\lambda (t2: T).(pc3 +c0 (lift h x1 t2) (THead (Bind Abst) u t))) (\lambda (t2: T).(ty3 g e x0 +t2)))))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H5: (eq T (THead +(Flat Appl) w v) (lift h x1 x0))).(\lambda (e: C).(\lambda (H6: (drop h x1 c0 +e)).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Flat +Appl) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T w (lift h x1 y0)))) +(\lambda (_: T).(\lambda (z: T).(eq T v (lift h x1 z)))) (ex2 T (\lambda (t2: +T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) w (THead (Bind Abst) u t)))) +(\lambda (t2: T).(ty3 g e x0 t2))) (\lambda (x2: T).(\lambda (x3: T).(\lambda +(H7: (eq T x0 (THead (Flat Appl) x2 x3))).(\lambda (H8: (eq T w (lift h x1 +x2))).(\lambda (H9: (eq T v (lift h x1 x3))).(eq_ind_r T (THead (Flat Appl) +x2 x3) (\lambda (t0: T).(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead +(Flat Appl) w (THead (Bind Abst) u t)))) (\lambda (t2: T).(ty3 g e t0 t2)))) +(let H10 \def (eq_ind T v (\lambda (t0: T).(\forall (x4: T).(\forall (x5: +nat).((eq T t0 (lift h x5 x4)) \to (\forall (e0: C).((drop h x5 c0 e0) \to +(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x5 t2) (THead (Bind Abst) u t))) +(\lambda (t2: T).(ty3 g e0 x4 t2))))))))) H4 (lift h x1 x3) H9) in (let H11 +\def (eq_ind T v (\lambda (t0: T).(ty3 g c0 t0 (THead (Bind Abst) u t))) H3 +(lift h x1 x3) H9) in (let H12 \def (eq_ind T w (\lambda (t0: T).(\forall (x4: T).(\forall (x5: nat).((eq T t0 (lift h x5 x4)) \to (\forall (e0: -C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x5 t2) -(THead (Bind Abst) u t))) (\lambda (t2: T).(ty3 g e0 x4 t2))))))))) H4 (lift -h x1 x3) H9) in (let H11 \def (eq_ind T v (\lambda (t0: T).(ty3 g c0 t0 -(THead (Bind Abst) u t))) H3 (lift h x1 x3) H9) in (let H12 \def (eq_ind T w -(\lambda (t0: T).(\forall (x4: T).(\forall (x5: nat).((eq T t0 (lift h x5 -x4)) \to (\forall (e0: C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t2: T).(pc3 -c0 (lift h x5 t2) u)) (\lambda (t2: T).(ty3 g e0 x4 t2))))))))) H2 (lift h x1 -x2) H8) in (let H13 \def (eq_ind T w (\lambda (t0: T).(ty3 g c0 t0 u)) H1 -(lift h x1 x2) H8) in (eq_ind_r T (lift h x1 x2) (\lambda (t0: T).(ex2 T -(\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) t0 (THead (Bind -Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl) x2 x3) t2)))) (let -H14 \def (H12 x2 x1 (refl_equal T (lift h x1 x2)) e H6) in (ex2_ind T -(\lambda (t2: T).(pc3 c0 (lift h x1 t2) u)) (\lambda (t2: T).(ty3 g e x2 t2)) -(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) (lift h x1 -x2) (THead (Bind Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl) -x2 x3) t2))) (\lambda (x4: T).(\lambda (H15: (pc3 c0 (lift h x1 x4) -u)).(\lambda (H16: (ty3 g e x2 x4)).(let H17 \def (H10 x3 x1 (refl_equal T -(lift h x1 x3)) e H6) in (ex2_ind T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) -(THead (Bind Abst) u t))) (\lambda (t2: T).(ty3 g e x3 t2)) (ex2 T (\lambda +C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x5 t2) u)) +(\lambda (t2: T).(ty3 g e0 x4 t2))))))))) H2 (lift h x1 x2) H8) in (let H13 +\def (eq_ind T w (\lambda (t0: T).(ty3 g c0 t0 u)) H1 (lift h x1 x2) H8) in +(eq_ind_r T (lift h x1 x2) (\lambda (t0: T).(ex2 T (\lambda (t2: T).(pc3 c0 +(lift h x1 t2) (THead (Flat Appl) t0 (THead (Bind Abst) u t)))) (\lambda (t2: +T).(ty3 g e (THead (Flat Appl) x2 x3) t2)))) (let H14 \def (H12 x2 x1 +(refl_equal T (lift h x1 x2)) e H6) in (ex2_ind T (\lambda (t2: T).(pc3 c0 +(lift h x1 t2) u)) (\lambda (t2: T).(ty3 g e x2 t2)) (ex2 T (\lambda (t2: +T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) (lift h x1 x2) (THead (Bind +Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl) x2 x3) t2))) +(\lambda (x4: T).(\lambda (H15: (pc3 c0 (lift h x1 x4) u)).(\lambda (H16: +(ty3 g e x2 x4)).(let H17 \def (H10 x3 x1 (refl_equal T (lift h x1 x3)) e H6) +in (ex2_ind T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Bind Abst) u +t))) (\lambda (t2: T).(ty3 g e x3 t2)) (ex2 T (\lambda (t2: T).(pc3 c0 (lift +h x1 t2) (THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)))) +(\lambda (t2: T).(ty3 g e (THead (Flat Appl) x2 x3) t2))) (\lambda (x5: +T).(\lambda (H18: (pc3 c0 (lift h x1 x5) (THead (Bind Abst) u t))).(\lambda +(H19: (ty3 g e x3 x5)).(ex3_2_ind T T (\lambda (u1: T).(\lambda (t2: T).(pr3 +e x5 (THead (Bind Abst) u1 t2)))) (\lambda (u1: T).(\lambda (_: T).(pr3 c0 u +(lift h x1 u1)))) (\lambda (_: T).(\lambda (t2: T).(\forall (b: B).(\forall +(u0: T).(pr3 (CHead c0 (Bind b) u0) t (lift h (S x1) t2)))))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl) x2 x3) t2))) -(\lambda (x5: T).(\lambda (H18: (pc3 c0 (lift h x1 x5) (THead (Bind Abst) u -t))).(\lambda (H19: (ty3 g e x3 x5)).(ex3_2_ind T T (\lambda (u1: T).(\lambda -(t2: T).(pr3 e x5 (THead (Bind Abst) u1 t2)))) (\lambda (u1: T).(\lambda (_: -T).(pr3 c0 u (lift h x1 u1)))) (\lambda (_: T).(\lambda (t2: T).(\forall (b: -B).(\forall (u0: T).(pr3 (CHead c0 (Bind b) u0) t (lift h (S x1) t2)))))) -(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) (lift h x1 -x2) (THead (Bind Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl) -x2 x3) t2))) (\lambda (x6: T).(\lambda (x7: T).(\lambda (H20: (pr3 e x5 -(THead (Bind Abst) x6 x7))).(\lambda (H21: (pr3 c0 u (lift h x1 -x6))).(\lambda (H22: ((\forall (b: B).(\forall (u0: T).(pr3 (CHead c0 (Bind -b) u0) t (lift h (S x1) x7)))))).(ex_ind T (\lambda (t0: T).(ty3 g e x5 t0)) -(ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) (lift h x1 -x2) (THead (Bind Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl) -x2 x3) t2))) (\lambda (x8: T).(\lambda (H23: (ty3 g e x5 x8)).(ex4_3_ind T T -T (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(pc3 e (THead (Bind Abst) -x6 t2) x8)))) (\lambda (_: T).(\lambda (t0: T).(\lambda (_: T).(ty3 g e x6 -t0)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (_: T).(ty3 g (CHead e (Bind -Abst) x6) x7 t2)))) (\lambda (t2: T).(\lambda (_: T).(\lambda (t3: T).(ty3 g -(CHead e (Bind Abst) x6) t2 t3)))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 +(\lambda (x6: T).(\lambda (x7: T).(\lambda (H20: (pr3 e x5 (THead (Bind Abst) +x6 x7))).(\lambda (H21: (pr3 c0 u (lift h x1 x6))).(\lambda (H22: ((\forall +(b: B).(\forall (u0: T).(pr3 (CHead c0 (Bind b) u0) t (lift h (S x1) +x7)))))).(ex_ind T (\lambda (t0: T).(ty3 g e x5 t0)) (ex2 T (\lambda (t2: +T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) (lift h x1 x2) (THead (Bind +Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl) x2 x3) t2))) +(\lambda (x8: T).(\lambda (H23: (ty3 g e x5 x8)).(let H_y \def (ty3_sred_pr3 +e x5 (THead (Bind Abst) x6 x7) H20 g x8 H23) in (ex3_2_ind T T (\lambda (t2: +T).(\lambda (_: T).(pc3 e (THead (Bind Abst) x6 t2) x8))) (\lambda (_: +T).(\lambda (t0: T).(ty3 g e x6 t0))) (\lambda (t2: T).(\lambda (_: T).(ty3 g +(CHead e (Bind Abst) x6) x7 t2))) (ex2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl) x2 x3) t2))) (\lambda (x9: T).(\lambda -(x10: T).(\lambda (x11: T).(\lambda (_: (pc3 e (THead (Bind Abst) x6 x9) -x8)).(\lambda (H25: (ty3 g e x6 x10)).(\lambda (H26: (ty3 g (CHead e (Bind -Abst) x6) x7 x9)).(\lambda (H27: (ty3 g (CHead e (Bind Abst) x6) x9 -x11)).(ex_intro2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) +(x10: T).(\lambda (_: (pc3 e (THead (Bind Abst) x6 x9) x8)).(\lambda (H25: +(ty3 g e x6 x10)).(\lambda (H26: (ty3 g (CHead e (Bind Abst) x6) x7 +x9)).(ex_intro2 T (\lambda (t2: T).(pc3 c0 (lift h x1 t2) (THead (Flat Appl) (lift h x1 x2) (THead (Bind Abst) u t)))) (\lambda (t2: T).(ty3 g e (THead (Flat Appl) x2 x3) t2)) (THead (Flat Appl) x2 (THead (Bind Abst) x6 x7)) (eq_ind_r T (THead (Flat Appl) (lift h x1 x2) (lift h x1 (THead (Bind Abst) @@ -397,9 +384,8 @@ Abst) x6 x7)) (lift_bind Abst x6 x7 h x1)) (lift h x1 x2) Appl) (lift h x1 H16 (pc3_gen_lift c0 x4 x6 h x1 (pc3_t u c0 (lift h x1 x4) H15 (lift h x1 x6) (pc3_pr3_r c0 u (lift h x1 x6) H21)) e H6)) x3 x7 (ty3_conv g e (THead (Bind Abst) x6 x7) (THead (Bind Abst) x6 x9) (ty3_bind g e x6 x10 H25 Abst x7 x9 -H26 x11 H27) x3 x5 H19 (pc3_pr3_r e x5 (THead (Bind Abst) x6 x7) -H20))))))))))) (ty3_gen_bind g Abst e x6 x7 x8 (ty3_sred_pr3 e x5 (THead -(Bind Abst) x6 x7) H20 g x8 H23))))) (ty3_correct g e x3 x5 H19))))))) +H26) x3 x5 H19 (pc3_pr3_r e x5 (THead (Bind Abst) x6 x7) H20))))))))) +(ty3_gen_bind g Abst e x6 x7 x8 H_y))))) (ty3_correct g e x3 x5 H19))))))) (pc3_gen_lift_abst c0 x5 t u h x1 H18 e H6))))) H17))))) H14)) w H8))))) x0 H7)))))) (lift_gen_flat Appl w v x0 h x1 H5)))))))))))))))) (\lambda (c0: C).(\lambda (t2: T).(\lambda (t3: T).(\lambda (H1: (ty3 g c0 t2 t3)).(\lambda @@ -414,40 +400,45 @@ x0 t4)))))))))).(\lambda (x0: T).(\lambda (x1: nat).(\lambda (H5: (eq T (drop h x1 c0 e)).(ex3_2_ind T T (\lambda (y0: T).(\lambda (z: T).(eq T x0 (THead (Flat Cast) y0 z)))) (\lambda (y0: T).(\lambda (_: T).(eq T t3 (lift h x1 y0)))) (\lambda (_: T).(\lambda (z: T).(eq T t2 (lift h x1 z)))) (ex2 T -(\lambda (t4: T).(pc3 c0 (lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e x0 -t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7: (eq T x0 (THead (Flat -Cast) x2 x3))).(\lambda (H8: (eq T t3 (lift h x1 x2))).(\lambda (H9: (eq T t2 -(lift h x1 x3))).(eq_ind_r T (THead (Flat Cast) x2 x3) (\lambda (t: T).(ex2 T -(\lambda (t4: T).(pc3 c0 (lift h x1 t4) t3)) (\lambda (t4: T).(ty3 g e t -t4)))) (let H10 \def (eq_ind T t3 (\lambda (t: T).(\forall (x4: T).(\forall -(x5: nat).((eq T t (lift h x5 x4)) \to (\forall (e0: C).((drop h x5 c0 e0) -\to (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x5 t4) t0)) (\lambda (t4: T).(ty3 -g e0 x4 t4))))))))) H4 (lift h x1 x2) H8) in (let H11 \def (eq_ind T t3 -(\lambda (t: T).(ty3 g c0 t t0)) H3 (lift h x1 x2) H8) in (let H12 \def -(eq_ind T t3 (\lambda (t: T).(\forall (x4: T).(\forall (x5: nat).((eq T t2 -(lift h x5 x4)) \to (\forall (e0: C).((drop h x5 c0 e0) \to (ex2 T (\lambda -(t4: T).(pc3 c0 (lift h x5 t4) t)) (\lambda (t4: T).(ty3 g e0 x4 t4))))))))) -H2 (lift h x1 x2) H8) in (let H13 \def (eq_ind T t3 (\lambda (t: T).(ty3 g c0 -t2 t)) H1 (lift h x1 x2) H8) in (eq_ind_r T (lift h x1 x2) (\lambda (t: -T).(ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) t)) (\lambda (t4: T).(ty3 g -e (THead (Flat Cast) x2 x3) t4)))) (let H14 \def (eq_ind T t2 (\lambda (t: -T).(ty3 g c0 t (lift h x1 x2))) H13 (lift h x1 x3) H9) in (let H15 \def -(eq_ind T t2 (\lambda (t: T).(\forall (x4: T).(\forall (x5: nat).((eq T t -(lift h x5 x4)) \to (\forall (e0: C).((drop h x5 c0 e0) \to (ex2 T (\lambda -(t4: T).(pc3 c0 (lift h x5 t4) (lift h x1 x2))) (\lambda (t4: T).(ty3 g e0 x4 -t4))))))))) H12 (lift h x1 x3) H9) in (let H16 \def (H15 x3 x1 (refl_equal T -(lift h x1 x3)) e H6) in (ex2_ind T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) -(lift h x1 x2))) (\lambda (t4: T).(ty3 g e x3 t4)) (ex2 T (\lambda (t4: -T).(pc3 c0 (lift h x1 t4) (lift h x1 x2))) (\lambda (t4: T).(ty3 g e (THead +(\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 t3))) (\lambda +(t4: T).(ty3 g e x0 t4))) (\lambda (x2: T).(\lambda (x3: T).(\lambda (H7: (eq +T x0 (THead (Flat Cast) x2 x3))).(\lambda (H8: (eq T t3 (lift h x1 +x2))).(\lambda (H9: (eq T t2 (lift h x1 x3))).(eq_ind_r T (THead (Flat Cast) +x2 x3) (\lambda (t: T).(ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead +(Flat Cast) t0 t3))) (\lambda (t4: T).(ty3 g e t t4)))) (let H10 \def (eq_ind +T t3 (\lambda (t: T).(\forall (x4: T).(\forall (x5: nat).((eq T t (lift h x5 +x4)) \to (\forall (e0: C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t4: T).(pc3 +c0 (lift h x5 t4) t0)) (\lambda (t4: T).(ty3 g e0 x4 t4))))))))) H4 (lift h +x1 x2) H8) in (let H11 \def (eq_ind T t3 (\lambda (t: T).(ty3 g c0 t t0)) H3 +(lift h x1 x2) H8) in (let H12 \def (eq_ind T t3 (\lambda (t: T).(\forall +(x4: T).(\forall (x5: nat).((eq T t2 (lift h x5 x4)) \to (\forall (e0: +C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x5 t4) t)) +(\lambda (t4: T).(ty3 g e0 x4 t4))))))))) H2 (lift h x1 x2) H8) in (let H13 +\def (eq_ind T t3 (\lambda (t: T).(ty3 g c0 t2 t)) H1 (lift h x1 x2) H8) in +(eq_ind_r T (lift h x1 x2) (\lambda (t: T).(ex2 T (\lambda (t4: T).(pc3 c0 +(lift h x1 t4) (THead (Flat Cast) t0 t))) (\lambda (t4: T).(ty3 g e (THead +(Flat Cast) x2 x3) t4)))) (let H14 \def (eq_ind T t2 (\lambda (t: T).(ty3 g +c0 t (lift h x1 x2))) H13 (lift h x1 x3) H9) in (let H15 \def (eq_ind T t2 +(\lambda (t: T).(\forall (x4: T).(\forall (x5: nat).((eq T t (lift h x5 x4)) +\to (\forall (e0: C).((drop h x5 c0 e0) \to (ex2 T (\lambda (t4: T).(pc3 c0 +(lift h x5 t4) (lift h x1 x2))) (\lambda (t4: T).(ty3 g e0 x4 t4))))))))) H12 +(lift h x1 x3) H9) in (let H16 \def (H15 x3 x1 (refl_equal T (lift h x1 x3)) +e H6) in (ex2_ind T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (lift h x1 x2))) +(\lambda (t4: T).(ty3 g e x3 t4)) (ex2 T (\lambda (t4: T).(pc3 c0 (lift h x1 +t4) (THead (Flat Cast) t0 (lift h x1 x2)))) (\lambda (t4: T).(ty3 g e (THead (Flat Cast) x2 x3) t4))) (\lambda (x4: T).(\lambda (H17: (pc3 c0 (lift h x1 x4) (lift h x1 x2))).(\lambda (H18: (ty3 g e x3 x4)).(let H19 \def (H10 x2 x1 (refl_equal T (lift h x1 x2)) e H6) in (ex2_ind T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) t0)) (\lambda (t4: T).(ty3 g e x2 t4)) (ex2 T (\lambda (t4: -T).(pc3 c0 (lift h x1 t4) (lift h x1 x2))) (\lambda (t4: T).(ty3 g e (THead -(Flat Cast) x2 x3) t4))) (\lambda (x5: T).(\lambda (_: (pc3 c0 (lift h x1 x5) -t0)).(\lambda (H21: (ty3 g e x2 x5)).(ex_intro2 T (\lambda (t4: T).(pc3 c0 -(lift h x1 t4) (lift h x1 x2))) (\lambda (t4: T).(ty3 g e (THead (Flat Cast) -x2 x3) t4)) x2 (pc3_refl c0 (lift h x1 x2)) (ty3_cast g e x3 x2 (ty3_conv g e +T).(pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 (lift h x1 x2)))) (\lambda +(t4: T).(ty3 g e (THead (Flat Cast) x2 x3) t4))) (\lambda (x5: T).(\lambda +(H20: (pc3 c0 (lift h x1 x5) t0)).(\lambda (H21: (ty3 g e x2 x5)).(ex_intro2 +T (\lambda (t4: T).(pc3 c0 (lift h x1 t4) (THead (Flat Cast) t0 (lift h x1 +x2)))) (\lambda (t4: T).(ty3 g e (THead (Flat Cast) x2 x3) t4)) (THead (Flat +Cast) x5 x2) (eq_ind_r T (THead (Flat Cast) (lift h x1 x5) (lift h x1 x2)) +(\lambda (t: T).(pc3 c0 t (THead (Flat Cast) t0 (lift h x1 x2)))) (pc3_head_1 +c0 (lift h x1 x5) t0 H20 (Flat Cast) (lift h x1 x2)) (lift h x1 (THead (Flat +Cast) x5 x2)) (lift_flat Cast x5 x2 h x1)) (ty3_cast g e x3 x2 (ty3_conv g e x2 x5 H21 x3 x4 H18 (pc3_gen_lift c0 x4 x2 h x1 H17 e H6)) x5 H21))))) H19))))) H16)))) t3 H8))))) x0 H7)))))) (lift_gen_flat Cast t3 t2 x0 h x1 H5))))))))))))))) c y x H0))))) H))))))). @@ -459,8 +450,8 @@ t1) \to (\forall (t2: T).((pr3 c t1 t2) \to (ty3 g c u t2))))))) \lambda (g: G).(\lambda (c: C).(\lambda (u: T).(\lambda (t1: T).(\lambda (H: (ty3 g c u t1)).(\lambda (t2: T).(\lambda (H0: (pr3 c t1 t2)).(ex_ind T (\lambda (t: T).(ty3 g c t1 t)) (ty3 g c u t2) (\lambda (x: T).(\lambda (H1: -(ty3 g c t1 x)).(ty3_conv g c t2 x (ty3_sred_pr3 c t1 t2 H0 g x H1) u t1 H -(pc3_pr3_r c t1 t2 H0)))) (ty3_correct g c u t1 H)))))))). +(ty3 g c t1 x)).(let H_y \def (ty3_sred_pr3 c t1 t2 H0 g x H1) in (ty3_conv g +c t2 x H_y u t1 H (pc3_pr3_r c t1 t2 H0))))) (ty3_correct g c u t1 H)))))))). theorem ty3_sconv_pc3: \forall (g: G).(\forall (c: C).(\forall (u1: T).(\forall (t1: T).((ty3 g c @@ -471,9 +462,9 @@ u2) \to (pc3 c t1 t2))))))))) (H: (ty3 g c u1 t1)).(\lambda (u2: T).(\lambda (t2: T).(\lambda (H0: (ty3 g c u2 t2)).(\lambda (H1: (pc3 c u1 u2)).(let H2 \def H1 in (ex2_ind T (\lambda (t: T).(pr3 c u1 t)) (\lambda (t: T).(pr3 c u2 t)) (pc3 c t1 t2) (\lambda (x: -T).(\lambda (H3: (pr3 c u1 x)).(\lambda (H4: (pr3 c u2 x)).(ty3_unique g c x -t1 (ty3_sred_pr3 c u1 x H3 g t1 H) t2 (ty3_sred_pr3 c u2 x H4 g t2 H0))))) -H2)))))))))). +T).(\lambda (H3: (pr3 c u1 x)).(\lambda (H4: (pr3 c u2 x)).(let H_y \def +(ty3_sred_pr3 c u2 x H4 g t2 H0) in (let H_y0 \def (ty3_sred_pr3 c u1 x H3 g +t1 H) in (ty3_unique g c x t1 H_y0 t2 H_y)))))) H2)))))))))). theorem ty3_sred_back: \forall (g: G).(\forall (c: C).(\forall (t1: T).(\forall (t0: T).((ty3 g c