---

Step * of Lemma es-empty-interface_wf

∀[Info,A:Type].  (Empty ∈ EClass(A))
BY
{ (Unfolds ``es-empty-interface eclass`` 0 THEN Auto) }

---

Latex:


\mforall{}[Info,A:Type].    (Empty  \mmember{}  EClass(A))


By

(Unfolds  ``es-empty-interface  eclass``  0  THEN  Auto)

---

Home Index