---

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