---

Step * of Lemma csm-ap-term-meaning_wf

No Annotations
∀[X,Y:⊢''']. ∀[s:cube_set_map{i''':l}(X; Y)]. ∀[t:cttTerm(Y)].  ((t)s ∈ cttTerm(X))
BY
{ (Intros
   THEN Unhide
   THEN RepeatFor 2 (D -1)
   THEN RepUR ``csm-ap-term-meaning ctt-term-meaning`` 0
   THEN MemCD
   THEN Try (Trivial)
   THEN Try ((IntSegCases (-1) THEN RepUR ``ctt-level-type`` 0 THEN Auto))
   THEN IntSegCases (-3)
   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{}[t:cttTerm(Y)].    ((t)s  \mmember{}  cttTerm(X))


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  RepeatFor  2  (D  -1)
  THEN  RepUR  ``csm-ap-term-meaning  ctt-term-meaning``  0
  THEN  MemCD
  THEN  Try  (Trivial)
  THEN  Try  ((IntSegCases  (-1)  THEN  RepUR  ``ctt-level-type``  0  THEN  Auto))
  THEN  IntSegCases  (-3)
  THEN  Eliminate  \mkleeneopen{}lvl\mkleeneclose{}\mcdot{}
  THEN  All  (RepUR  ``ctt-level-type``)
  THEN  Auto)

---

Home Index