DEFINITION subst1_gen_lift_eq()
TYPE =
       ∀t:T
         .∀u:T
           .∀x:T
             .∀h:nat
               .∀d:nat
                 .∀i:nat
                   .le d i
                     →(lt i (plus d h)
                          →(subst1 i u (lift h d t) x)→(eq T x (lift h d t)))
BODY =
        assume t: T
        assume u: T
        assume x: T
        assume h: nat
        assume d: nat
        assume i: nat
        suppose H: le d i
        suppose H0: lt i (plus d h)
        suppose H1: subst1 i u (lift h d t) x
          we proceed by induction on H1 to prove eq T x (lift h d t)
             case subst1_refl : ⇒
                the thesis becomes eq T (lift h d t) (lift h d t)
                   by (refl_equal . .)
eq T (lift h d t) (lift h d t)
             case subst1_single : t2:T H2:subst0 i u (lift h d t) t2 ⇒
                the thesis becomes eq T t2 (lift h d t)
                   by (subst0_gen_lift_false . . . . . . H H0 H2 .)
eq T t2 (lift h d t)
          we proved eq T x (lift h d t)
       we proved 
          ∀t:T
            .∀u:T
              .∀x:T
                .∀h:nat
                  .∀d:nat
                    .∀i:nat
                      .le d i
                        →(lt i (plus d h)
                             →(subst1 i u (lift h d t) x)→(eq T x (lift h d t)))