Step
*
of Lemma
integ_dom_wf
IntegDom{i} ∈ 𝕌'
BY
{ Unfold `integ_dom` 0 THEN Auto }
Latex:
Latex:
IntegDom\{i\}  \mmember{}  \mBbbU{}'
By
Latex:
Unfold  `integ\_dom`  0  THEN  Auto
Home
Index