DEFINITION wadd_O()
TYPE =
∀
n:
nat
.(
eq
nat
(
wadd
λ
:
nat
.
O
O
n)
O
)
BODY =
Show proof