---

Step * of Lemma es-loc_wf

∀[the_es:EO]. ∀[e:E].  (loc(e) ∈ Id)
BY
{ (Auto THEN D 1 THEN (DRecord 1⋅ THENA Auto) THEN All (Fold `es-E`) THEN ProveWfLemma) }

---

Latex:


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


By

(Auto  THEN  D  1  THEN  (DRecord  1\mcdot{}  THENA  Auto)  THEN  All  (Fold  `es-E`)  THEN  ProveWfLemma)

---

Home Index