---

Step * 2 of Lemma es-local-le-pred_wf


1. Info : Type
2. P : es:EO+(Info) ─→ E ─→ 𝔹
3. ∀es:EO+(Info). ∀e:E.  (≤(P) es e ∈ bag({e:E| ↑(P es e)} ))
⊢ ≤(P) ∈ EClass({e:E| ↑(P es e)} )
BY
{ (Unfold `eclass` 0 THEN (ExtWith [`a'] [⌈Top ─→ Top⌉]⋅ THENA Auto)) }

1
1. Info : Type
2. P : es:EO+(Info) ─→ E ─→ 𝔹
3. ∀es:EO+(Info). ∀e:E.  (≤(P) es e ∈ bag({e:E| ↑(P es e)} ))
4. a : EO+(Info)
⊢ ≤(P) a ∈ e:E ─→ bag({e:E| ↑(P a e)} )

---

Latex:

---

Latex:

1.  Info  :  Type
2.  P  :  es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbB{}
3.  \mforall{}es:EO+(Info).  \mforall{}e:E.    (\mleq{}(P)  es  e  \mmember{}  bag(\{e:E|  \muparrow{}(P  es  e)\}  ))
\mvdash{}  \mleq{}(P)  \mmember{}  EClass(\{e:E|  \muparrow{}(P  es  e)\}  )


By

---

Latex:
(Unfold  `eclass`  0  THEN  (ExtWith  [`a']  [\mkleeneopen{}Top  {}\mrightarrow{}  Top\mkleeneclose{}]\mcdot{}  THENA  Auto))

---

Home Index