---

Step * of Lemma transEquiv-trans_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}]. ∀[p:{G ⊢ _:(Path_c𝕌 A B)}].  (transEquivFun(p) ∈ {G ⊢ _:(decode(A) ⟶ decode(B))})
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].  \mforall{}[p:\{G  \mvdash{}  \_:(Path\_c\mBbbU{}  A  B)\}].
    (transEquivFun(p)  \mmember{}  \{G  \mvdash{}  \_:(decode(A)  {}\mrightarrow{}  decode(B))\})


By

---

Latex:
ProveWfLemma

---

Home Index