---

Step * of Lemma ctt-context-term-mng_wf

No Annotations
∀[X:?CubicalContext]. ∀[t:CttTerm].  (ctt-context-term-mng{i:l}(X;t) ∈ [[X;t]])
BY
{ (Intros
   THEN Unhide
   THEN Unfold `ctt-context-term-mng` 0
   THEN BLemma `wfterm-accum_wf_ctt1`
   THEN ((RepUR ``ctt_meaning ctt-meaning-type isvarterm varterm`` 0
          THEN RepeatFor 3 ((FunExt THENW Auto))
          THEN Reduce 0
          THEN RepeatFor 2 (MemCD))
   ORELSE Auto
   )) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:?CubicalContext].  \mforall{}[t:CttTerm].    (ctt-context-term-mng\{i:l\}(X;t)  \mmember{}  [[X;t]])


By

---

Latex:
(Intros
  THEN  Unhide
  THEN  Unfold  `ctt-context-term-mng`  0
  THEN  BLemma  `wfterm-accum\_wf\_ctt1`
  THEN  ((RepUR  ``ctt\_meaning  ctt-meaning-type  isvarterm  varterm``  0
                THEN  RepeatFor  3  ((FunExt  THENW  Auto))
                THEN  Reduce  0
                THEN  RepeatFor  2  (MemCD))
  ORELSE  Auto
  ))

---

Home Index