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 =
Show proof