---

Step * of Lemma is-latest-val

∀[Info:Type]. ∀es:EO+(Info). ∀[T:Type]. ∀X:EClass(T). ∀e:E.  (↑e ∈b (X)- ⇐⇒ ∃e':E. (e' ≤loc e  ∧ (↑e' ∈b X)))
BY
{ Auto }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. [T] : Type
4. X : EClass(T)@i'
5. e : E@i
6. ↑e ∈b (X)-@i
⊢ ∃e':E. (e' ≤loc e  ∧ (↑e' ∈b X))

2
1. Info : Type
2. es : EO+(Info)@i'
3. T : Type
4. X : EClass(T)@i'
5. e : E@i
6. ∃e':E. (e' ≤loc e  ∧ (↑e' ∈b X))@i
⊢ ↑e ∈b (X)-

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}[T:Type].  \mforall{}X:EClass(T).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  (X)\msupminus{}  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e':E.  (e'  \mleq{}loc  e    \mwedge{}  (\muparrow{}e'  \mmember{}\msubb{}  X)))


By

---

Latex:
Auto

---

Home Index