---

Step * of Lemma ctt-level-type-cumulativity

No Annotations
∀[X:⊢''']. ∀[lvl:ℕ4].  ({X ⊢lvl _} ⊆r ctt-level-type{i':l}(X; lvl))
BY
{ (Intros THEN Unfold `ctt-level-type` 0 THEN Unhide THEN OnVar `lvl' IntSegCases THEN Reduce 0 THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:\mvdash{}'''].  \mforall{}[lvl:\mBbbN{}4].    (\{X  \mvdash{}lvl  \_\}  \msubseteq{}r  ctt-level-type\{i':l\}(X;  lvl))


By

---

Latex:
(Intros
  THEN  Unfold  `ctt-level-type`  0
  THEN  Unhide
  THEN  OnVar  `lvl'  IntSegCases
  THEN  Reduce  0
  THEN  Auto)

---

Home Index