---

Step * of Lemma es-eq_wf

∀[es:EO]. (es-eq(es) ∈ EqDecider(E))
BY
{ ProveWfLemma }

1
1. es : EO
⊢ λe1,e2. (loc(e1) = loc(e2) ∧b (¬bes-locless(es;e1;e2)) ∧b (¬bes-locless(es;e2;e1))) ∈ EqDecider(E)

---

Latex:


\mforall{}[es:EO].  (es-eq(es)  \mmember{}  EqDecider(E))


By

ProveWfLemma

---

Home Index