---

Step * of Lemma es-is-interface-p-first

∀[Info:Type]. ∀es:EO+(Info). ∀[A:Type]. ∀Ias:EClass(A) List. ∀e:E.  (↑e ∈b first-eclass(Ias) ⇐⇒ (∃I∈Ias. ↑e ∈b I))
BY
{ ((UnivCD THENA Auto) THEN RWO "in-first-eclass" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info)
        \mforall{}[A:Type].  \mforall{}Ias:EClass(A)  List.  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  first-eclass(Ias)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}I\mmember{}Ias.  \muparrow{}e  \mmember{}\msubb{}  I))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RWO  "in-first-eclass"  0  THEN  Auto)

---

Home Index