DEFINITION wadd_O()
TYPE =
       ∀n:nat.(eq nat (wadd λ:nat.O O n) O)
BODY =
       assume n: nat
          we proceed by induction on n to prove eq nat (wadd λ:nat.O O n) O
             case O : ⇒
                the thesis becomes eq nat (wadd λ:nat.O O O) O
                   by (refl_equal . .)
                   we proved eq nat O O
eq nat (wadd λ:nat.O O O) O
             case S : n0:nat ⇒
                the thesis becomes eq nat (wadd λ:nat.O O (S n0)) O
                () by induction hypothesis we know eq nat (wadd λ:nat.O O n0) O
                   by (refl_equal . .)
                   we proved eq nat O O
eq nat (wadd λ:nat.O O (S n0)) O
          we proved eq nat (wadd λ:nat.O O n) O
       we proved ∀n:nat.(eq nat (wadd λ:nat.O O n) O)