---

Step * of Lemma es-base-E_wf

∀[es:EO]. (es-base-E(es) ∈ Type)
BY
{ (Auto THEN D -1 THEN (DRecord (-2) THENA Auto) THEN ProveWfLemma) }

---

Latex:


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


By

(Auto  THEN  D  -1  THEN  (DRecord  (-2)  THENA  Auto)  THEN  ProveWfLemma)

---

Home Index