---

Step * of Lemma first-eclass-val

∀[Info,A:Type].
  ∀Xs:EClass(A) List. ∀es:EO+(Info). ∀e:E.
    (∃X∈Xs. (↑e ∈b X) ∧ (first-eclass(Xs)(e) = X(e) ∈ A)) supposing ↑e ∈b first-eclass(Xs)
BY
{ (InductionOnList THEN Auto THEN DupHyp (-1) THEN (RWW "in-first-eclass l_exists_cons" (-1) THENA Auto)) }

1
1. [Info] : Type
2. [A] : Type
3. es : EO+(Info)@i'
4. e : E@i
5. ↑e ∈b first-eclass([])
6. ↑e ∈b first-eclass([])
⊢ (∃X∈[]. (↑e ∈b X) ∧ (first-eclass([])(e) = X(e) ∈ A))

2
1. [Info] : Type
2. [A] : Type
3. u : EClass(A)@i'
4. v : EClass(A) List@i'
5. ∀es:EO+(Info). ∀e:E.  (∃X∈v. (↑e ∈b X) ∧ (first-eclass(v)(e) = X(e) ∈ A)) supposing ↑e ∈b first-eclass(v)@i'
6. es : EO+(Info)@i'
7. e : E@i
8. ↑e ∈b first-eclass([u / v])
9. (↑e ∈b u) ∨ (∃X∈v. ↑e ∈b X)
⊢ (∃X∈[u / v]. (↑e ∈b X) ∧ (first-eclass([u / v])(e) = X(e) ∈ A))

---

Latex:

---

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


By

---

Latex:
(InductionOnList
  THEN  Auto
  THEN  DupHyp  (-1)
  THEN  (RWW  "in-first-eclass  l\_exists\_cons"  (-1)  THENA  Auto))

---

Home Index