---

Step * of Lemma es-locless_wf

∀[es:EO]. ∀[e,e':E].  (es-locless(es;e;e') ∈ 𝔹)
BY
{ (Auto THEN D 1 THEN (DRecord 1 THENA Auto) THEN All (RepUR ``es-E es-locless``) THEN Auto) }

---

Latex:


\mforall{}[es:EO].  \mforall{}[e,e':E].    (es-locless(es;e;e')  \mmember{}  \mBbbB{})


By

(Auto  THEN  D  1  THEN  (DRecord  1  THENA  Auto)  THEN  All  (RepUR  ``es-E  es-locless``)  THEN  Auto)

---

Home Index