---

Step * 1 of Lemma interface_predicate_set_lemma


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

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

---

Latex:



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


By

Try  (RW  (AddrC  [1]  (UnfoldC  `es-interface-predicate`  ANDTHENC  ReduceC))  0)\mcdot{}

---

Home Index