---

Step * 1 of Lemma in-first-eclass


1. [Info] : Type
2. [A] : Type
⊢ ∀es:EO+(Info). ∀e:E.  (↑e ∈b first-eclass([]) ⇐⇒ False)
BY
{ (RepUR ``first-eclass in-eclass`` 0 THEN Auto)⋅ }

---

Latex:

---

Latex:

1.  [Info]  :  Type
2.  [A]  :  Type
\mvdash{}  \mforall{}es:EO+(Info).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  first-eclass([])  \mLeftarrow{}{}\mRightarrow{}  False)


By

---

Latex:
(RepUR  ``first-eclass  in-eclass``  0  THEN  Auto)\mcdot{}

---

Home Index