---

Step * 1 3 of Lemma first-class-val

.....wf..... 
1. Info : Type
2. A : Type
3. u : EClass(A)@i'
4. v : EClass(A) List@i'
⊢ ∀es:EO+(Info). ∀e:E.
    ((↑e ∈b first-class(v))
    ⇒ ((↑e ∈b v[index-of-first X in v.e ∈b X - 1]) ∧ (first-class(v)(e) = v[index-of-first X in v.e ∈b X - 1](e) ∈ A)))
  ∈ ℙ'
BY
{ (RepeatFor 3 (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;v]⋅
   THEN Auto) }

---

Latex:


.....wf..... 
1.  Info  :  Type
2.  A  :  Type
3.  u  :  EClass(A)@i'
4.  v  :  EClass(A)  List@i'
\mvdash{}  \mforall{}es:EO+(Info).  \mforall{}e:E.
        ((\muparrow{}e  \mmember{}\msubb{}  first-class(v))
        {}\mRightarrow{}  ((\muparrow{}e  \mmember{}\msubb{}  v[index-of-first  X  in  v.e  \mmember{}\msubb{}  X  -  1])
              \mwedge{}  (first-class(v)(e)  =  v[index-of-first  X  in  v.e  \mmember{}\msubb{}  X  -  1](e))))  \mmember{}  \mBbbP{}'


By

(RepeatFor  3  (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;v]\mcdot{}
  THEN  Auto)

---

Home Index