---

Step * of Lemma equivTerm_wf

No Annotations
∀[G:j⊢]. ∀[A,B:{G ⊢ _:c𝕌}].  (equivTerm(G;A;B) ∈ {G ⊢ _:c𝕌})
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[G:j\mvdash{}].  \mforall{}[A,B:\{G  \mvdash{}  \_:c\mBbbU{}\}].    (equivTerm(G;A;B)  \mmember{}  \{G  \mvdash{}  \_:c\mBbbU{}\})


By

---

Latex:
ProveWfLemma

---

Home Index