---

Step * of Lemma cubical-universe-cumulativity

No Annotations
∀[X:j⊢]. ({X ⊢ _:c𝕌} ⊆r {X ⊢ _:c𝕌'})
BY
{ (Intros
   THEN (D 0 THENA (BLemma `istype-cubical-universe-term` THEN Auto))
   THEN (BLemma `cubical-universe-cumulativity2` THENA Auto)) }

---

Latex:

---

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


By

---

Latex:
(Intros
  THEN  (D  0  THENA  (BLemma  `istype-cubical-universe-term`  THEN  Auto))
  THEN  (BLemma  `cubical-universe-cumulativity2`  THENA  Auto))

---

Home Index