Step
*
of Lemma
nc-1-lemma2
No Annotations
∀j:ℕ. ((j1) j ~ {{}})
BY
{ ((Auto THEN RepUR ``nc-1`` 0) THEN AutoSplit) }
Latex:
Latex:
No  Annotations
\mforall{}j:\mBbbN{}.  ((j1)  j  \msim{}  \{\{\}\})
By
Latex:
((Auto  THEN  RepUR  ``nc-1``  0)  THEN  AutoSplit)
Home
Index