DEFINITION subst1_confluence_lift()
TYPE =
       ∀t0:T
         .∀t1:T
           .∀u:T
             .∀i:nat
               .(subst1 i u t0 (lift (S O) i t1))→∀t2:T.(subst1 i u t0 (lift (S O) i t2))→(eq T t1 t2)
BODY =
Show proof