Step
*
of Lemma
univ-comp_wf
No Annotations
ā[G:jā¢]. (univ-comp{i:l}() ā G ā¢ CompOp(cš))
BY
{ (Intro THEN Subst' univ-comp{i:l}() ~ cfun-to-cop(G;cš;compU()) 0 THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}[G:j\mvdash{}]. (univ-comp\{i:l\}() \mmember{} G \mvdash{} CompOp(c\mBbbU{}))
By
Latex:
(Intro THEN Subst' univ-comp\{i:l\}() \msim{} cfun-to-cop(G;c\mBbbU{};compU()) 0 THEN Auto)
Home
Index