---

Step * of Lemma member-implies-classrel

∀[Info,T:Type]. ∀[X:EClass(T)]. ∀[es:EO+(Info)]. ∀[e:E].  ↓∃v:T. v ∈ X(e) supposing ↑e ∈b X
BY
{ (Auto
   THEN Unfold `member-eclass` (-1)
   THEN (RW assert_pushdownC (-1) THENA Auto)
   THEN (Assert ⌈0 < #(X es e)⌉⋅ THENA Auto')
   THEN RWO "bag-size-bag-member" (-1)
   THEN Auto
   THEN Fold `classrel` (-1)
   THEN D 0
   THEN Trivial) }

---

Latex:


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


By

(Auto
  THEN  Unfold  `member-eclass`  (-1)
  THEN  (RW  assert\_pushdownC  (-1)  THENA  Auto)
  THEN  (Assert  \mkleeneopen{}0  <  \#(X  es  e)\mkleeneclose{}\mcdot{}  THENA  Auto')
  THEN  RWO  "bag-size-bag-member"  (-1)
  THEN  Auto
  THEN  Fold  `classrel`  (-1)
  THEN  D  0
  THEN  Trivial)

---

Home Index