---

Step * of Lemma l_all-interface-predecessors

∀[Info:Type]
  ∀es:EO+(Info). ∀X:EClass(Top).  ∀[P:E(X) ⟶ ℙ]. ∀e:E. ((∀e'∈≤(X)(e).P[e']) ⇐⇒ ∀e':E(X). (e' ≤loc e  ⇒ P[e']))
BY
{ WithCumulativity(((UnivCD THENA Auto) THEN RWO "l_all_iff" 0 THEN Auto)) }

1
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. [P] : E(X) ⟶ ℙ
5. e : E@i
6. ∀e':{a:E(X)| loc(a) = loc(e) ∈ Id} . ((e' ∈ ≤(X)(e)) ⇒ P[e'])@i
7. e' : E(X)@i
8. e' ≤loc e @i
⊢ P[e']

2
1. [Info] : Type
2. es : EO+(Info)@i'
3. X : EClass(Top)@i'
4. [P] : E(X) ⟶ ℙ
5. e : E@i
6. ∀e':E(X). (e' ≤loc e  ⇒ P[e'])@i
7. e' : {a:E(X)| loc(a) = loc(e) ∈ Id} @i
8. (e' ∈ ≤(X)(e))@i
⊢ P[e']

---

Latex:

---

Latex:
\mforall{}[Info:Type]
    \mforall{}es:EO+(Info).  \mforall{}X:EClass(Top).
        \mforall{}[P:E(X)  {}\mrightarrow{}  \mBbbP{}].  \mforall{}e:E.  ((\mforall{}e'\mmember{}\mleq{}(X)(e).P[e'])  \mLeftarrow{}{}\mRightarrow{}  \mforall{}e':E(X).  (e'  \mleq{}loc  e    {}\mRightarrow{}  P[e']))


By

---

Latex:
WithCumulativity(((UnivCD  THENA  Auto)  THEN  RWO  "l\_all\_iff"  0  THEN  Auto))

---

Home Index