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