Step
*
of Lemma
nim_sum0_lemma
∀y:Top. (nim-sum(0;y) ~ y)
BY
{ (UnivCD THENA Auto) }
1
1. y : Top
⊢ nim-sum(0;y) ~ y
Latex:
Latex:
\mforall{}y:Top.  (nim-sum(0;y)  \msim{}  y)
By
Latex:
(UnivCD  THENA  Auto)
Home
Index