---

Step * of Lemma es-locless-wf-base

∀[the_es:EO]. ∀[e,e':es-base-E(the_es)].  (es-locless(the_es;e;e') ∈ 𝔹)
BY
{ (RepeatFor 3 ((D 0 THENA Auto))
   THEN All (Unfold `es-base-E`)
   THEN (D 1 THEN (DRecord 1 THENA Auto) THEN ProveWfLemma)⋅) }

---

Latex:


\mforall{}[the$_{es}$:EO].  \mforall{}[e,e':es-base-E(the$_{es}$)].    (es-locles\000Cs(the$_{es}$;e;e')  \mmember{}  \mBbbB{})


By

(RepeatFor  3  ((D  0  THENA  Auto))
  THEN  All  (Unfold  `es-base-E`)
  THEN  (D  1  THEN  (DRecord  1  THENA  Auto)  THEN  ProveWfLemma)\mcdot{})

---

Home Index