---

Step * of Lemma cubical-term_wf-universe

No Annotations
∀X:j⊢. ({X ⊢ _:c𝕌} ∈ 𝕌{[i' | j']})
BY
{ ((Intro THEN InstLemma `cubical-term_wf` [⌜parm{j}⌝;⌜parm{i'}⌝]⋅) THEN BHyp -1 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}X:j\mvdash{}.  (\{X  \mvdash{}  \_:c\mBbbU{}\}  \mmember{}  \mBbbU{}\{[i'  |  j']\})


By

---

Latex:
((Intro  THEN  InstLemma  `cubical-term\_wf`  [\mkleeneopen{}parm\{j\}\mkleeneclose{};\mkleeneopen{}parm\{i'\}\mkleeneclose{}]\mcdot{})  THEN  BHyp  -1  THEN  Auto)

---

Home Index