DEFINITION nat_double_ind()
TYPE =
       ∀R:nat→nat→Prop
         .∀n:nat.(R O n)
           →(∀n:nat.(R (S n) O)
                →(∀n:nat.∀m:nat.(R n m)→(R (S n) (S m)))→∀n:nat.∀m:nat.(R n m))
BODY =
Show proof