---

Step * 1 1 of Lemma first-class-val

.....wf..... 
1. Info : Type
2. A : Type
⊢ λL.∀es:EO+(Info). ∀e:E.
       ((↑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))) ∈ (EClass(A) List) ─→ ℙ'
BY
{ (RepeatFor 4 (MemCD)
   THEN Try (CompleteAuto)
   THEN (FLemma `is-first-class2` [-1] THENA Auto)
   THEN Auto
   THEN InstLemma `first_index_bounds` [⌈parm{i'}⌉;EClass(A);λ2X.e ∈b X;L]⋅
   THEN Auto) }

---

Latex:


.....wf..... 
1.  Info  :  Type
2.  A  :  Type
\mvdash{}  \mlambda{}L.\mforall{}es:EO+(Info).  \mforall{}e:E.
              ((\muparrow{}e  \mmember{}\msubb{}  first-class(L))
              {}\mRightarrow{}  ((\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))))  \mmember{}  (EClass(A)  List)  {}\mrightarrow{}  \mBbbP{}'


By

(RepeatFor  4  (MemCD)
  THEN  Try  (CompleteAuto)
  THEN  (FLemma  `is-first-class2`  [-1]  THENA  Auto)
  THEN  Auto
  THEN  InstLemma  `first\_index\_bounds`  [\mkleeneopen{}parm\{i'\}\mkleeneclose{};EClass(A);\mlambda{}\msubtwo{}X.e  \mmember{}\msubb{}  X;L]\mcdot{}
  THEN  Auto)

---

Home Index