DEFINITION nat_dec()
TYPE =
       ∀n1:nat.∀n2:nat.(or (eq nat n1 n2) (eq nat n1 n2)→∀P:Prop.P)
BODY =
Show proof