---

Step * 1 of Lemma is-first-class2


1. Info : Type
2. A : Type
3. L : EClass(A) List
4. es : EO+(Info)
5. e : E
6. ↑e ∈b first-class(L) ⇐⇒ (∃X∈L. ↑e ∈b X)
⊢ uiff(↑e ∈b first-class(L);0 < index-of-first X in L.e ∈b X)
BY
{ (RWO "first_index-positive" 0 THEN Auto)⋅ }

---

Latex:



1.  Info  :  Type
2.  A  :  Type
3.  L  :  EClass(A)  List
4.  es  :  EO+(Info)
5.  e  :  E
6.  \muparrow{}e  \mmember{}\msubb{}  first-class(L)  \mLeftarrow{}{}\mRightarrow{}  (\mexists{}X\mmember{}L.  \muparrow{}e  \mmember{}\msubb{}  X)
\mvdash{}  uiff(\muparrow{}e  \mmember{}\msubb{}  first-class(L);0  <  index-of-first  X  in  L.e  \mmember{}\msubb{}  X)


By

(RWO  "first\_index-positive"  0  THEN  Auto)\mcdot{}

---

Home Index