DEFINITION neq_eq_e()
TYPE =
       ∀i:nat
         .∀j:nat
           .∀P:Prop.((not (eq nat i j))→P)→((eq nat i j)→P)→P
BODY =
        assume i: nat
        assume j: nat
        assume P: Prop
        suppose H: (not (eq nat i j))→P
        suppose H0: (eq nat i j)→P
          (o) 
             by (eq_nat_dec . .)
or (not (eq nat i j)) (eq nat i j)
          end of o
          we proceed by induction on o to prove P
             case or_introl ⇒
                the thesis becomes the hypothesis H
             case or_intror ⇒
                the thesis becomes the hypothesis H0
          we proved P
       we proved 
          ∀i:nat
            .∀j:nat
              .∀P:Prop.((not (eq nat i j))→P)→((eq nat i j)→P)→P