---

Step * of Lemma ctt-type-meaning-subtype

No Annotations
∀[X:⊢''']. (cttType(X) ⊆r ctt-type-meaning1{i:l}(X))
BY
{ (Intro
   THEN (D 0 THENA Auto)
   THEN D -1
   THEN IntSegCases  (-2)
   THEN Eliminate⌜lvl⌝⋅
   THEN Reduce -2
   THEN RepUR ``ctt-type-meaning1`` 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:\mvdash{}'''].  (cttType(X)  \msubseteq{}r  ctt-type-meaning1\{i:l\}(X))


By

---

Latex:
(Intro
  THEN  (D  0  THENA  Auto)
  THEN  D  -1
  THEN  IntSegCases    (-2)
  THEN  Eliminate\mkleeneopen{}lvl\mkleeneclose{}\mcdot{}
  THEN  Reduce  -2
  THEN  RepUR  ``ctt-type-meaning1``  0
  THEN  Auto)

---

Home Index