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()) 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