---

Step * of Lemma is-first-class2

∀[Info,A:Type]. ∀[L:EClass(A) List]. ∀[es:EO+(Info)]. ∀[e:E].
  uiff(↑e ∈b first-class(L);0 < index-of-first X in L.e ∈b X)
BY
{ (InstLemma `is-first-class` [] THEN RepeatFor 5 (ParallelLast')) }

1
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)

---

Latex:


\mforall{}[Info,A:Type].  \mforall{}[L:EClass(A)  List].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    uiff(\muparrow{}e  \mmember{}\msubb{}  first-class(L);0  <  index-of-first  X  in  L.e  \mmember{}\msubb{}  X)


By

(InstLemma  `is-first-class`  []  THEN  RepeatFor  5  (ParallelLast'))

---

Home Index