---

Step * of Lemma ctt-eq_wf

No Annotations
∀[a,b:CttTerm].  (ctt-eq{i:l}(a;b) ∈ ℙ')
BY
{ ProveWfLemma }

---

Latex:

---

Latex:
No  Annotations
\mforall{}[a,b:CttTerm].    (ctt-eq\{i:l\}(a;b)  \mmember{}  \mBbbP{}')


By

---

Latex:
ProveWfLemma

---

Home Index