---

Step * of Lemma name-deq_wf

NameDeq ∈ EqDecider(Name)
BY
{ (Unfold `name` 0 THEN ProveWfLemma) }

---

Latex:

---

Latex:
NameDeq  \mmember{}  EqDecider(Name)


By

---

Latex:
(Unfold  `name`  0  THEN  ProveWfLemma)

---

Home Index