---

Step * 1 of Lemma es-interface-events-append


1. Info : Type
2. es : EO+(Info)
3. X : EClass(Top)
4. L1 : E List
5. L2 : E List
⊢ filter(λe.e ∈b X;L1 @ L2) ~ eclass-events(es;X;L1) @ eclass-events(es;X;L2)
BY
{ (((RWO "filter_append_sq" 0 THENA Auto) THEN Fold `eclass-events` 0) THEN Auto) }

---

Latex:

---

Latex:

1.  Info  :  Type
2.  es  :  EO+(Info)
3.  X  :  EClass(Top)
4.  L1  :  E  List
5.  L2  :  E  List
\mvdash{}  filter(\mlambda{}e.e  \mmember{}\msubb{}  X;L1  @  L2)  \msim{}  eclass-events(es;X;L1)  @  eclass-events(es;X;L2)


By

---

Latex:
(((RWO  "filter\_append\_sq"  0  THENA  Auto)  THEN  Fold  `eclass-events`  0)  THEN  Auto)

---

Home Index