Step
*
of Lemma
cc-snd_wf-level-type
No Annotations
∀[X:⊢''']. ∀[lvl:ℕ4]. ∀[T:{X ⊢lvl _}]. (q ∈ {X.T ⊢ _:(T)p})
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
THEN IntSegCases (-1)
THEN RepUR ``ctt-level-type`` 0
THEN (D 0 THENA Auto)
THEN MemCD
THEN Auto) }
Latex:
Latex:
No Annotations
\mforall{}[X:\mvdash{}''']. \mforall{}[lvl:\mBbbN{}4]. \mforall{}[T:\{X \mvdash{}lvl \_\}]. (q \mmember{} \{X.T \mvdash{} \_:(T)p\})
By
Latex:
(RepeatFor 2 ((D 0 THENA Auto))
THEN IntSegCases (-1)
THEN RepUR ``ctt-level-type`` 0
THEN (D 0 THENA Auto)
THEN MemCD
THEN Auto)
Home
Index