DEFINITION subst1_gen_lift_lt()
TYPE =
       ∀u:T
         .∀t1:T
           .∀x:T
             .∀i:nat
               .∀h:nat
                 .∀d:nat
                   .subst1 i (lift h d u) (lift h (S (plus i d)) t1) x
                     →ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst1 i u t1 t2
BODY =
        assume u: T
        assume t1: T
        assume x: T
        assume i: nat
        assume h: nat
        assume d: nat
        suppose H: subst1 i (lift h d u) (lift h (S (plus i d)) t1) x
          we proceed by induction on H to prove ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst1 i u t1 t2
             case subst1_refl : ⇒
                the thesis becomes 
                ex2
                  T
                  λt2:T.eq T (lift h (S (plus i d)) t1) (lift h (S (plus i d)) t2)
                  λt2:T.subst1 i u t1 t2
                   (h1) 
                      by (refl_equal . .)
eq T (lift h (S (plus i d)) t1) (lift h (S (plus i d)) t1)
                   end of h1
                   (h2) 
                      by (subst1_refl . . .)
subst1 i u t1 t1
                   end of h2
                   by (ex_intro2 . . . . h1 h2)

                      ex2
                        T
                        λt2:T.eq T (lift h (S (plus i d)) t1) (lift h (S (plus i d)) t2)
                        λt2:T.subst1 i u t1 t2
             case subst1_single : t2:T H0:subst0 i (lift h d u) (lift h (S (plus i d)) t1) t2 ⇒
                the thesis becomes ex2 T λt3:T.eq T t2 (lift h (S (plus i d)) t3) λt3:T.subst1 i u t1 t3
                   by (subst0_gen_lift_lt . . . . . . H0)
                   we proved ex2 T λt2:T.eq T t2 (lift h (S (plus i d)) t2) λt2:T.subst0 i u t1 t2
                   we proceed by induction on the previous result to prove ex2 T λt3:T.eq T t2 (lift h (S (plus i d)) t3) λt3:T.subst1 i u t1 t3
                      case ex_intro2 : x0:T H1:eq T t2 (lift h (S (plus i d)) x0) H2:subst0 i u t1 x0 ⇒
                         the thesis becomes ex2 T λt3:T.eq T t2 (lift h (S (plus i d)) t3) λt3:T.subst1 i u t1 t3
                            by (subst1_single . . . . H2)
                            we proved subst1 i u t1 x0
                            by (ex_intro2 . . . . H1 previous)
ex2 T λt3:T.eq T t2 (lift h (S (plus i d)) t3) λt3:T.subst1 i u t1 t3
ex2 T λt3:T.eq T t2 (lift h (S (plus i d)) t3) λt3:T.subst1 i u t1 t3
          we proved ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst1 i u t1 t2
       we proved 
          ∀u:T
            .∀t1:T
              .∀x:T
                .∀i:nat
                  .∀h:nat
                    .∀d:nat
                      .subst1 i (lift h d u) (lift h (S (plus i d)) t1) x
                        →ex2 T λt2:T.eq T x (lift h (S (plus i d)) t2) λt2:T.subst1 i u t1 t2