---

Step * 1 of Lemma prior-latest-val


1. Info : Type
2. T : Type
3. X : EClass(T)
⊢ ∀es:EO+(Info). ∀e:E.  (↑e ∈b (X)' ⇐⇒ ↑e ∈b ((X)-)')
BY
{ (RWW "is-prior-val is-latest-val" 0 THEN Auto THEN ExRepD) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  T  :  Type
3.  X  :  EClass(T)
\mvdash{}  \mforall{}es:EO+(Info).  \mforall{}e:E.    (\muparrow{}e  \mmember{}\msubb{}  (X)'  \mLeftarrow{}{}\mRightarrow{}  \muparrow{}e  \mmember{}\msubb{}  ((X)\msupminus{})')


By

---

Latex:
(RWW  "is-prior-val  is-latest-val"  0  THEN  Auto  THEN  ExRepD)

---

Home Index