DEFINITION eq_nat_dec()
TYPE =
       ∀i:nat.∀j:nat.(or (not (eq nat i j)) (eq nat i j))
BODY =
Show proof