---

Step * of Lemma path-eta_wf

No Annotations
∀[G:j⊢]. ∀[A:{G ⊢ _}]. ∀[pth:{G ⊢ _:Path(A)}].  (path-eta(pth) ∈ {G.𝕀 ⊢ _:(A)p})
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A:\{G  \mvdash{}  \_\}].  \mforall{}[pth:\{G  \mvdash{}  \_:Path(A)\}].    (path-eta(pth)  \mmember{}  \{G.\mBbbI{}  \mvdash{}  \_:(A)p\})


By

---

Latex:
ProveWfLemma

---

Home Index