DEFINITION subst1_lift_ge()
TYPE =
       ∀t1:T
         .∀t2:T
           .∀u:T
             .∀i:nat
               .∀h:nat
                 .subst1 i u t1 t2
                   →∀d:nat.(le d i)→(subst1 (plus i h) u (lift h d t1) (lift h d t2))
BODY =
        assume t1: T
        assume t2: T
        assume u: T
        assume i: nat
        assume h: nat
        suppose H: subst1 i u t1 t2
          we proceed by induction on H to prove ∀d:nat.(le d i)→(subst1 (plus i h) u (lift h d t1) (lift h d t2))
             case subst1_refl : ⇒
                the thesis becomes ∀d:nat.(le d i)→(subst1 (plus i h) u (lift h d t1) (lift h d t1))
                    assume d: nat
                    suppose : le d i
                      by (subst1_refl . . .)
                      we proved subst1 (plus i h) u (lift h d t1) (lift h d t1)
∀d:nat.(le d i)→(subst1 (plus i h) 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:(le d i).(subst1 (plus i h) u (lift h d t1) (lift h d t3))
                    assume d: nat
                    suppose H1: le d i
                      by (subst0_lift_ge . . . . . H0 . H1)
                      we proved subst0 (plus i h) u (lift h d t1) (lift h d t3)
                      by (subst1_single . . . . previous)
                      we proved subst1 (plus i h) u (lift h d t1) (lift h d t3)
∀d:nat.∀H1:(le d i).(subst1 (plus i h) u (lift h d t1) (lift h d t3))
          we proved ∀d:nat.(le d i)→(subst1 (plus i h) u (lift h d t1) (lift h d t2))
       we proved 
          ∀t1:T
            .∀t2:T
              .∀u:T
                .∀i:nat
                  .∀h:nat
                    .subst1 i u t1 t2
                      →∀d:nat.(le d i)→(subst1 (plus i h) u (lift h d t1) (lift h d t2))