---

Step * of Lemma cname_deq_wf

CnameDeq ∈ EqDecider(Cname)
BY
{ (Unfold `coordinate_name` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
CnameDeq  \mmember{}  EqDecider(Cname)


By

---

Latex:
(Unfold  `coordinate\_name`  0  THEN  ProveWfLemma)

---

Home Index