---

Step * of Lemma istype-cubical-term-closed-type

No Annotations
∀[X:j⊢]. ∀[T:{ * ⊢ _}].  istype({X ⊢ _:closed-type-to-type(T)})
BY
{ (Intros THEN D -1 THEN D -2 THEN RepUR ``closed-type-to-type cubical-term`` 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[T:\{  *  \mvdash{}  \_\}].    istype(\{X  \mvdash{}  \_:closed-type-to-type(T)\})


By

---

Latex:
(Intros  THEN  D  -1  THEN  D  -2  THEN  RepUR  ``closed-type-to-type  cubical-term``  0  THEN  Auto)

---

Home Index