DEFINITION neq_eq_e()
TYPE =
       ∀i:nat
         .∀j:nat
           .∀P:Prop.((not (eq nat i j))→P)→((eq nat i j)→P)→P
BODY =
Show proof