---

Step * of Lemma in-first-eclass

∀[Info,A:Type].  ∀Xs:EClass(A) List. ∀es:EO+(Info). ∀e:E.  (↑e ∈b first-eclass(Xs) ⇐⇒ (∃X∈Xs. ↑e ∈b X))
BY
{ (At ⌜𝕌'⌝InductionOnLast⋅ THEN (RWW "l_exists_cons l_exists_nil" 0 THENA Auto)) }

1
1. [Info] : Type
2. [A] : Type
⊢ ∀es:EO+(Info). ∀e:E.  (↑e ∈b first-eclass([]) ⇐⇒ False)

2
1. [Info] : Type
2. [A] : Type
3. Xs : EClass(A) List@i'
4. ¬↑null(Xs)
5. ||Xs|| ≥ 1 
6. ∀es:EO+(Info). ∀e:E.  (↑e ∈b first-eclass(firstn(||Xs|| - 1;Xs)) ⇐⇒ (∃X∈firstn(||Xs|| - 1;Xs). ↑e ∈b X))
⊢ ∀es:EO+(Info). ∀e:E.
    (↑e ∈b first-eclass(firstn(||Xs|| - 1;Xs) @ [last(Xs)]) ⇐⇒ (∃X∈firstn(||Xs|| - 1;Xs) @ [last(Xs)]. ↑e ∈b X))

---

Latex:

---

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


By

---

Latex:
(At  \mkleeneopen{}\mBbbU{}'\mkleeneclose{}InductionOnLast\mcdot{}  THEN  (RWW  "l\_exists\_cons  l\_exists\_nil"  0  THENA  Auto))

---

Home Index