---

Step * of Lemma no-prior-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[T:Type]. ∀[X:EClass(T)]. ∀[e:E].
  uiff(¬↑e ∈b (X)';∀[e':E]. ¬↑e' ∈b X supposing (e' <loc e))
BY
{ WithCumulativity ((UnivCD THENA Auto)
                    THEN RWO "is-prior-val" 0
                    THEN Auto
                    THEN Try ((ParallelOp (-3) THEN With ⌜e'⌝ (D 0)⋅ THEN Auto)))⋅ }

1
1. Info : Type
2. es : EO+(Info)
3. T : Type
4. X : EClass(T)
5. e : E
6. ∀[e':E]. ¬↑e' ∈b X supposing (e' <loc e)
⊢ ¬(∃e':E. ((e' <loc e) ∧ (↑e' ∈b X)))

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[e:E].
    uiff(\mneg{}\muparrow{}e  \mmember{}\msubb{}  (X)';\mforall{}[e':E].  \mneg{}\muparrow{}e'  \mmember{}\msubb{}  X  supposing  (e'  <loc  e))


By

---

Latex:
WithCumulativity  ((UnivCD  THENA  Auto)
                                    THEN  RWO  "is-prior-val"  0
                                    THEN  Auto
                                    THEN  Try  ((ParallelOp  (-3)  THEN  With  \mkleeneopen{}e'\mkleeneclose{}  (D  0)\mcdot{}  THEN  Auto)))\mcdot{}

---

Home Index