---

Step * 1 of Lemma primed-classrel


1. Info : Type
2. T : Type
3. X : EClass(T)
4. es : EO+(Info)
5. v : T
6. e : E
7. v ∈ Prior(X)(e)
⊢ ↓∃e'<e.v ∈ X(e') ∧ ∀e''<e.∀w:T. (w ∈ X(e'') ⇒ e'' ≤loc e' )
BY
{ (MoveToConcl (-1)
   THEN RepUR ``classrel primed-class`` 0
   THEN (GenConclAtAddr[1;3;1] THENA Auto)
   THEN Reduce (-2)
   THEN D -2
   THEN Reduce 0
   THEN Auto
   THEN Try ((FLemma `bag-member-empty` [-1] THEN Auto))) }

1
1. Info : Type
2. T : Type
3. X : EClass(T)
4. es : EO+(Info)
5. v : T
6. e : E
7. x : ∃e':{E| ((e' <loc e) ∧ (↑0 <z #(X es e')) ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑0 <z #(X es e'')))))}@i
8. (last(λe'.0 <z #(X es e')) e)
= (inl x)
∈ ((∃e':{E| ((e' <loc e)
            ∧ (↑((λe'.0 <z #(X es e')) e'))
            ∧ (∀e'':E. ((e' <loc e'') ⇒ (e'' <loc e) ⇒ (¬↑((λe'.0 <z #(X es e')) e'')))))})
  ∨ (¬(∃e':{E| ((e' <loc e) ∧ (↑((λe'.0 <z #(X es e')) e')))})))@i
9. v ↓∈ X es x@i
⊢ ↓∃e'<e.v ↓∈ X es e' ∧ ∀e''<e.∀w:T. (w ↓∈ X es e'' ⇒ e'' ≤loc e' )

---

Latex:

---

Latex:

1.  Info  :  Type
2.  T  :  Type
3.  X  :  EClass(T)
4.  es  :  EO+(Info)
5.  v  :  T
6.  e  :  E
7.  v  \mmember{}  Prior(X)(e)
\mvdash{}  \mdownarrow{}\mexists{}e'<e.v  \mmember{}  X(e')  \mwedge{}  \mforall{}e''<e.\mforall{}w:T.  (w  \mmember{}  X(e'')  {}\mRightarrow{}  e''  \mleq{}loc  e'  )


By

---

Latex:
(MoveToConcl  (-1)
  THEN  RepUR  ``classrel  primed-class``  0
  THEN  (GenConclAtAddr[1;3;1]  THENA  Auto)
  THEN  Reduce  (-2)
  THEN  D  -2
  THEN  Reduce  0
  THEN  Auto
  THEN  Try  ((FLemma  `bag-member-empty`  [-1]  THEN  Auto)))

---

Home Index