Step
*
of Lemma
add_nat_wf
∀[i,j:ℕ].  (i + j ∈ ℕ)
BY
{ Auto' }
Latex:
Latex:
\mforall{}[i,j:\mBbbN{}].    (i  +  j  \mmember{}  \mBbbN{})
By
Latex:
Auto'
Home
Index