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