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)