---

Step * of Lemma closed-term-to-term_wf

No Annotations
∀[T:{ * ⊢ _}]. ∀[t:closed-cubical-term(T)]. ∀[X:j⊢].  (closed-term-to-term(t) ∈ {X ⊢ _:closed-type-to-type(T)})
BY
{ (ProveWfLemma
   THEN RepeatFor 2 (D 1)
   THEN RepUR ``closed-cubical-term`` -2
   THEN RepUR ``closed-type-to-type`` 0
   THEN All Reduce
   THEN MemTypeCD
   THEN Reduce 0
   THEN Auto) }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[T:\{  *  \mvdash{}  \_\}].  \mforall{}[t:closed-cubical-term(T)].  \mforall{}[X:j\mvdash{}].
    (closed-term-to-term(t)  \mmember{}  \{X  \mvdash{}  \_:closed-type-to-type(T)\})


By

---

Latex:
(ProveWfLemma
  THEN  RepeatFor  2  (D  1)
  THEN  RepUR  ``closed-cubical-term``  -2
  THEN  RepUR  ``closed-type-to-type``  0
  THEN  All  Reduce
  THEN  MemTypeCD
  THEN  Reduce  0
  THEN  Auto)

---

Home Index