---

Step * of Lemma es-dom_wf

∀[es:EO]. (es-dom(es) ∈ es-base-E(es) ─→ 𝔹)
BY
{ (Unfold `es-base-E` 0 THEN (Auto THEN Try (Unfold `es-dom` 0) THEN (D 1 THEN DRecord 1 THEN Auto)⋅)⋅) }

---

Latex:


\mforall{}[es:EO].  (es-dom(es)  \mmember{}  es-base-E(es)  {}\mrightarrow{}  \mBbbB{})


By

(Unfold  `es-base-E`  0
  THEN  (Auto  THEN  Try  (Unfold  `es-dom`  0)  THEN  (D  1  THEN  DRecord  1  THEN  Auto)\mcdot{})\mcdot{}
  )

---

Home Index