---

Step * of Lemma istype-cubical-universe-term

No Annotations
∀X:j⊢. istype({X ⊢ _:c𝕌})
BY
{ (Intro THEN GenConclTerm ⌜{X ⊢ _:c𝕌}⌝⋅ THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:j\mvdash{}.  istype(\{X  \mvdash{}  \_:c\mBbbU{}\})


By

---

Latex:
(Intro  THEN  GenConclTerm  \mkleeneopen{}\{X  \mvdash{}  \_:c\mBbbU{}\}\mkleeneclose{}\mcdot{}  THEN  Auto)

---

Home Index