---

Step * of Lemma is-prior-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
{ ((UnivCD THENA Auto)
   THEN Unfold `es-prior-val` 0
   THEN RW (AddrC [1;1] UnfoldTopAbC) 0
   THEN Reduce 0
   THEN AutoSplit
   THEN (RWW "es-is-prior-interface" (-1) THEN Auto)⋅) }

---

Latex:

---

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


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  Unfold  `es-prior-val`  0
  THEN  RW  (AddrC  [1;1]  UnfoldTopAbC)  0
  THEN  Reduce  0
  THEN  AutoSplit
  THEN  (RWW  "es-is-prior-interface"  (-1)  THEN  Auto)\mcdot{})

---

Home Index