Step
*
1
1
of Lemma
nat-retractible
∀x:ℕ. (if (x) < (0)  then ⊥  else x = x ∈ ℕ)
BY
{ Auto }
Latex:
Latex:
\mforall{}x:\mBbbN{}.  (if  (x)  <  (0)    then  \mbot{}    else  x  =  x)
By
Latex:
Auto
Home
Index