---

Step * 2 of Lemma first-class-val

.....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] ∈ 𝔹
BY
{ ((FLemma `is-first-class2` [-2] THEN Auto)
   THEN InstLemma `first_index_bounds` [⌜parm{i'}⌝;⌜EClass(A)⌝;⌜λ2X.e ∈b X⌝;⌜L⌝]⋅
   THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
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)
7.  \muparrow{}e  \mmember{}\msubb{}  L[index-of-first  X  in  L.e  \mmember{}\msubb{}  X  -  1]
\mvdash{}  e  \mmember{}\msubb{}  L[index-of-first  X  in  L.e  \mmember{}\msubb{}  X  -  1]  \mmember{}  \mBbbB{}


By

---

Latex:
((FLemma  `is-first-class2`  [-2]  THEN  Auto)
  THEN  InstLemma  `first\_index\_bounds`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};\mkleeneopen{}EClass(A)\mkleeneclose{};\mkleeneopen{}\mlambda{}\msubtwo{}X.e  \mmember{}\msubb{}  X\mkleeneclose{};\mkleeneopen{}L\mkleeneclose{}]\mcdot{}
  THEN  Auto)

---

Home Index