---

Step * of Lemma es-E_wf

∀[the_es:EO]. (E ∈ Type)
BY
{ (Auto THEN D 1 THEN (DRecord 1 THENA Auto) THEN ProveWfLemma)⋅ }

---

Latex:


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


By

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

---

Home Index