DEFINITION subst1_lift_lt()
TYPE =
       ∀t1:T
         .∀t2:T
           .∀u:T
             .∀i:nat
               .subst1 i u t1 t2
                 →∀d:nat
                      .lt i d
                        →∀h:nat.(subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2))
BODY =
        assume t1: T
        assume t2: T
        assume u: T
        assume i: nat
        suppose H: subst1 i u t1 t2
          we proceed by induction on H to prove 
             ∀d:nat
               .lt i d
                 →∀h:nat.(subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2))
             case subst1_refl : ⇒
                the thesis becomes 
                ∀d:nat
                  .lt i d
                    →∀h:nat.(subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t1))
                    assume d: nat
                    suppose : lt i d
                    assume h: nat
                      by (subst1_refl . . .)
                      we proved subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t1)

                      ∀d:nat
                        .lt i d
                          →∀h:nat.(subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t1))
             case subst1_single : t3:T H0:subst0 i u t1 t3 ⇒
                the thesis becomes 
                ∀d:nat
                  .∀H1:lt i d
                    .∀h:nat.(subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t3))
                    assume d: nat
                    suppose H1: lt i d
                    assume h: nat
                      by (subst0_lift_lt . . . . H0 . H1 .)
                      we proved subst0 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t3)
                      by (subst1_single . . . . previous)
                      we proved subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t3)

                      ∀d:nat
                        .∀H1:lt i d
                          .∀h:nat.(subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t3))
          we proved 
             ∀d:nat
               .lt i d
                 →∀h:nat.(subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2))
       we proved 
          ∀t1:T
            .∀t2:T
              .∀u:T
                .∀i:nat
                  .subst1 i u t1 t2
                    →∀d:nat
                         .lt i d
                           →∀h:nat.(subst1 i (lift h (minus d (S i)) u) (lift h d t1) (lift h d t2))