---

Step * of Lemma es-loc-wf-base

∀[the_es:EO]. ∀[e:es-base-E(the_es)].  (loc(e) ∈ Id)
BY
{ (RepeatFor 2 ((D 0 THENA Auto)) THEN D 1 THEN (DRecord 1⋅ THENA Auto) THEN ProveWfLemma)⋅ }

---

Latex:


\mforall{}[the$_{es}$:EO].  \mforall{}[e:es-base-E(the$_{es}$)].    (loc(e)  \mmember{}  Id)


By

(RepeatFor  2  ((D  0  THENA  Auto))  THEN  D  1  THEN  (DRecord  1\mcdot{}  THENA  Auto)  THEN  ProveWfLemma)\mcdot{}

---

Home Index