---

Step * 1 1 of Lemma es-interface-le-pred

.....wf..... 
1. Info : Type
2. P : es:EO+(Info) ─→ E ─→ ℙ
3. ∀es:EO+(Info). ∀e:E.  Dec(P es e)@i'
4. es : EO+(Info)@i'
5. e : E@i
6. a : E
7. es-p-le-pred(es;P es) e a
⊢ a ∈ {e:E| P es e} 
BY
{ (RepUR ``es-p-le-pred`` (-1) THEN Auto) }

---

Latex:

---

Latex:
.....wf..... 
1.  Info  :  Type
2.  P  :  es:EO+(Info)  {}\mrightarrow{}  E  {}\mrightarrow{}  \mBbbP{}
3.  \mforall{}es:EO+(Info).  \mforall{}e:E.    Dec(P  es  e)@i'
4.  es  :  EO+(Info)@i'
5.  e  :  E@i
6.  a  :  E
7.  es-p-le-pred(es;P  es)  e  a
\mvdash{}  a  \mmember{}  \{e:E|  P  es  e\} 


By

---

Latex:
(RepUR  ``es-p-le-pred``  (-1)  THEN  Auto)

---

Home Index