Step
*
of Lemma
atomxnat_subtype_varname
No Annotations
(Atom × ℕ) ⊆r varname()
BY
{ (Unfold `varname` 0 THEN Auto) }
Latex:
Latex:
No  Annotations
(Atom  \mtimes{}  \mBbbN{})  \msubseteq{}r  varname()
By
Latex:
(Unfold  `varname`  0  THEN  Auto)
Home
Index