---

Step * of Lemma maname-deq_wf

maname-deq() ∈ EqDecider(MaName)
BY
{ (Unfolds ``maname-deq MaName`` 0 THEN Auto) }

---

Latex:

---

Latex:
maname-deq()  \mmember{}  EqDecider(MaName)


By

---

Latex:
(Unfolds  ``maname-deq  MaName``  0  THEN  Auto)

---

Home Index