---

Step * of Lemma csm-ap-type_wf-level-type

No Annotations
∀[X,Y:⊢''']. ∀[s:cube_set_map{i''':l}(X; Y)]. ∀[lvl:ℕ4]. ∀[T:{Y ⊢lvl _}].  ((T)s ∈ X ⊢lvl )
BY
{ (Auto THEN IntSegCases (-2) THEN Eliminate ⌜lvl⌝⋅ THEN All (RepUR ``ctt-level-type``) THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X,Y:\mvdash{}'''].  \mforall{}[s:cube\_set\_map\{i''':l\}(X;  Y)].  \mforall{}[lvl:\mBbbN{}4].  \mforall{}[T:\{Y  \mvdash{}lvl  \_\}].    ((T)s  \mmember{}  X  \mvdash{}lvl  )


By

---

Latex:
(Auto  THEN  IntSegCases  (-2)  THEN  Eliminate  \mkleeneopen{}lvl\mkleeneclose{}\mcdot{}  THEN  All  (RepUR  ``ctt-level-type``)  THEN  Auto)

---

Home Index