---

Step * of Lemma es-interface-filter-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A:Type]. ∀[X:EClass(A)]. ∀[P:A ─→ 𝔹]. ∀[e:E].
  X|a.P[a](e) ~ X(e) supposing ↑e ∈b X|a.P[a]
BY
{ (RepUR ``in-eclass eclass eclass-val  
           es-interface-filter eclass-compose1`` 0⋅
   THEN RepeatFor 6 ((D 0 THENA Auto))
   THEN AutoSplit
   THEN ElimBagSizeOne'
   THEN RepUR ``bag-filter single-bag bag-only bag-size`` 0
   THEN AutoSplit) }

---

Latex:

---

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].  \mforall{}[A:Type].  \mforall{}[X:EClass(A)].  \mforall{}[P:A  {}\mrightarrow{}  \mBbbB{}].  \mforall{}[e:E].
    X|a.P[a](e)  \msim{}  X(e)  supposing  \muparrow{}e  \mmember{}\msubb{}  X|a.P[a]


By

---

Latex:
(RepUR  ``in-eclass  eclass  eclass-val   
                  es-interface-filter  eclass-compose1``  0\mcdot{}
  THEN  RepeatFor  6  ((D  0  THENA  Auto))
  THEN  AutoSplit
  THEN  ElimBagSizeOne'
  THEN  RepUR  ``bag-filter  single-bag  bag-only  bag-size``  0
  THEN  AutoSplit)

---

Home Index