DEFINITION subst1_confluence_neq()
TYPE =
       ∀t0:T
         .∀t1:T
           .∀u1:T
             .∀i1:nat
               .subst1 i1 u1 t0 t1
                 →∀t2:T.∀u2:T.∀i2:nat.(subst1 i2 u2 t0 t2)→(not (eq nat i1 i2))→(ex2 T λt:T.subst1 i2 u2 t1 t λt:T.subst1 i1 u1 t2 t)
BODY =
Show proof