---

Step * of Lemma term-to-pathtype_wf

No Annotations
∀[X:j⊢]. ∀[A:{X ⊢ _}].  ∀a:{X.𝕀 ⊢ _:(A)p}. (<>a ∈ {X ⊢ _:Path(A)})
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[X:j\mvdash{}].  \mforall{}[A:\{X  \mvdash{}  \_\}].    \mforall{}a:\{X.\mBbbI{}  \mvdash{}  \_:(A)p\}.  (<>a  \mmember{}  \{X  \mvdash{}  \_:Path(A)\})


By

---

Latex:
ProveWfLemma

---

Home Index