---

Step * of Lemma var-term-meaning_wf

No Annotations
∀[X:⊢''']. ∀[lvl:ℕ4]. ∀[T:{X ⊢lvl _}].  (var-term-meaning(lvl;T) ∈ cttTerm(X.T))
BY
{ (InstLemma `cube-context-adjoin_wf-level-type` []
   THEN RepeatFor 3 (ParallelLast')
   THEN (Unhide
         THEN (InstLemma `csm-ap-type_wf-level-type` [⌜X.T⌝;⌜X⌝;⌜p⌝;⌜lvl⌝;⌜T⌝]⋅ THENA Auto)
         THEN (InstLemma `cc-snd_wf-level-type` [⌜X⌝;⌜lvl⌝;⌜T⌝]⋅ THENA Auto))
   THEN ProveWfLemma) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:\mvdash{}'''].  \mforall{}[lvl:\mBbbN{}4].  \mforall{}[T:\{X  \mvdash{}lvl  \_\}].    (var-term-meaning(lvl;T)  \mmember{}  cttTerm(X.T))


By

---

Latex:
(InstLemma  `cube-context-adjoin\_wf-level-type`  []
  THEN  RepeatFor  3  (ParallelLast')
  THEN  (Unhide
              THEN  (InstLemma  `csm-ap-type\_wf-level-type`  [\mkleeneopen{}X.T\mkleeneclose{};\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}p\mkleeneclose{};\mkleeneopen{}lvl\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto)
              THEN  (InstLemma  `cc-snd\_wf-level-type`  [\mkleeneopen{}X\mkleeneclose{};\mkleeneopen{}lvl\mkleeneclose{};\mkleeneopen{}T\mkleeneclose{}]\mcdot{}  THENA  Auto))
  THEN  ProveWfLemma)

---

Home Index