---

Step * of Lemma member-eclass-iff-size

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E].  (↑e ∈b X ⇐⇒ 0 < #(X es e))
BY
{ (Unfold `member-eclass` 0
   THEN Auto
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN Auto') }

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].    (\muparrow{}e  \mmember{}\msubb{}  X  \mLeftarrow{}{}\mRightarrow{}  0  <  \#(X  es  e))


By

(Unfold  `member-eclass`  0
  THEN  Auto
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  Auto')

---

Home Index