---

Step * of Lemma classrel-implies-member

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E]. ∀[v:T].  ↑e ∈b X supposing v ∈ X(e)
BY
{ (Auto
   THEN Unfold `member-eclass` 0
   THEN (RW assert_pushdownC 0 THENA Auto)
   THEN (D 0 THENA Auto)
   THEN Unfold `classrel` (-2)
   THEN FLemma `bag-member-size` [-2]
   THEN Auto) }

---

Latex:


\mforall{}[Info,T:Type].  \mforall{}[X:EClass(T)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].  \mforall{}[v:T].    \muparrow{}e  \mmember{}\msubb{}  X  supposing  v  \mmember{}  X(e)


By

(Auto
  THEN  Unfold  `member-eclass`  0
  THEN  (RW  assert\_pushdownC  0  THENA  Auto)
  THEN  (D  0  THENA  Auto)
  THEN  Unfold  `classrel`  (-2)
  THEN  FLemma  `bag-member-size`  [-2]
  THEN  Auto)

---

Home Index