---

Step * 1 1 of Lemma interface_predicate_set_lemma


1. X : Top@i
2. es : Top@i
⊢ {e:E| ↑e ∈b X}  ~ E(X)
BY
{ Try (RW (AddrC [2] (UnfoldC `es-E-interface`)) 0)⋅ }

1
1. X : Top@i
2. es : Top@i
⊢ {e:E| ↑e ∈b X}  ~ {e:E| ↑e ∈b X} 

---

Latex:



1.  X  :  Top@i
2.  es  :  Top@i
\mvdash{}  \{e:E|  \muparrow{}e  \mmember{}\msubb{}  X\}    \msim{}  E(X)


By

Try  (RW  (AddrC  [2]  (UnfoldC  `es-E-interface`))  0)\mcdot{}

---

Home Index