---

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

No Annotations
∀[X,Y:⊢''']. ∀[s:cube_set_map{i''':l}(X; Y)]. ∀[lvl:ℕ4]. ∀[T:{Y ⊢lvl _}]. ∀[t:{Y ⊢ _:T}].  ((t)s ∈ {X ⊢ _:(T)s})
BY
{ ((RepeatFor 5 (Intro)
    THEN (InstLemma `cubical-term_wf-level-type` [⌜Y⌝;⌜lvl⌝;⌜T⌝]⋅ THENA Auto)
    THEN Intro
    THEN Unhide)
   THEN IntSegCases (-4)
   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  \_\}].  \mforall{}[t:\{Y  \mvdash{}  \_:T\}].
    ((t)s  \mmember{}  \{X  \mvdash{}  \_:(T)s\})


By

---

Latex:
((RepeatFor  5  (Intro)
    THEN  (InstLemma  `cubical-term\_wf-level-type`  [\mkleeneopen{}Y\mkleeneclose{};\mkleeneopen{}lvl\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)
    THEN  Intro
    THEN  Unhide)
  THEN  IntSegCases  (-4)
  THEN  Eliminate  \mkleeneopen{}lvl\mkleeneclose{}\mcdot{}
  THEN  All  (RepUR  ``ctt-level-type``)
  THEN  Auto)

---

Home Index