DEFINITION subst0_gen_lift_false()
TYPE =
       ∀t:T
         .∀u:T
           .∀x:T
             .∀h:nat
               .∀d:nat
                 .∀i:nat
                   .le d i
                     →(lt i (plus d h))→(subst0 i u (lift h d t) x)→∀P:Prop.P
BODY =
Show proof