---

Step * of Lemma first-class-val

∀[Info,A:Type]. ∀[L:EClass(A) List]. ∀[es:EO+(Info)]. ∀[e:E].
  (↑e ∈b L[index-of-first X in L.e ∈b X - 1]) ∧ (first-class(L)(e) = L[index-of-first X in L.e ∈b X - 1](e) ∈ A) 
  supposing ↑e ∈b first-class(L)
BY
{ RemoveUniform1 Auto Auto }

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)
⊢ (↑e ∈b L[index-of-first X in L.e ∈b X - 1]) ∧ (first-class(L)(e) = L[index-of-first X in L.e ∈b X - 1](e) ∈ A)

2
.....wf..... 
1. Info : Type
2. A : Type
3. L : EClass(A) List
4. es : EO+(Info)
5. e : E
6. ↑e ∈b first-class(L)
7. ↑e ∈b L[index-of-first X in L.e ∈b X - 1]
⊢ e ∈b L[index-of-first X in L.e ∈b X - 1] ∈ 𝔹

---

Latex:


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


By

RemoveUniform1  Auto  Auto

---

Home Index