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 =
        assume R: nat→nat→Prop
        suppose H: ∀n:nat.(R O n)
        suppose H0: ∀n:nat.(R (S n) O)
        suppose H1: ∀n:nat.∀m:nat.(R n m)→(R (S n) (S m))
        assume n: nat
          we proceed by induction on n to prove ∀m:nat.(R n m)
             case O : ⇒
                the thesis becomes the hypothesis H
             case S : n0:nat ⇒
                the thesis becomes ∀m:nat.(R (S n0) m)
                (H2) by induction hypothesis we know ∀m:nat.(R n0 m)
                   assume m: nat
                      we proceed by induction on m to prove R (S n0) m
                         case O : ⇒
                            the thesis becomes R (S n0) O
                               by (H0 .)
R (S n0) O
                         case S : n1:nat ⇒
                            the thesis becomes R (S n0) (S n1)
                            () by induction hypothesis we know R (S n0) n1
                               by (H2 .)
                               we proved R n0 n1
                               by (H1 . . previous)
R (S n0) (S n1)
                      we proved R (S n0) m
∀m:nat.(R (S n0) m)
          we proved ∀m:nat.(R n m)
       we proved 
          ∀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))