---

Step * of Lemma not-list-member-not-bag-member

∀[T:Type]. ∀[L:T List]. ∀[x:T].  ((¬(x ∈ L)) ⇒ (¬x ↓∈ L))
BY
{ ((UnivCD THENA Auto)⋅
   THEN ListInd (-3)
   THEN Auto
   THEN (D 0 THENA Auto)
   THEN BagMemberD (-1)
   THEN Auto
   THEN (RWO "cons_member" (-2) THENA Auto)
   THEN (RWO "not_over_or" (-2) THENA Auto)
   THEN Auto
   THEN (D (-4) THENA Auto)
   THEN RepeatFor 2 (D (-2))
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}[L:T  List].  \mforall{}[x:T].    ((\mneg{}(x  \mmember{}  L))  {}\mRightarrow{}  (\mneg{}x  \mdownarrow{}\mmember{}  L))


By

---

Latex:
((UnivCD  THENA  Auto)\mcdot{}
  THEN  ListInd  (-3)
  THEN  Auto
  THEN  (D  0  THENA  Auto)
  THEN  BagMemberD  (-1)
  THEN  Auto
  THEN  (RWO  "cons\_member"  (-2)  THENA  Auto)
  THEN  (RWO  "not\_over\_or"  (-2)  THENA  Auto)
  THEN  Auto
  THEN  (D  (-4)  THENA  Auto)
  THEN  RepeatFor  2  (D  (-2))
  THEN  Auto)

---

Home Index