---

Step * of Lemma bag-member-list-member

∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀L:T List. ∀b:bag(T). ∀x:T.  ((L = b ∈ bag(T)) ⇒ x ↓∈ b ⇒ (x ∈ L))))
BY
{ ((UnivCD THENA Auto)
   THEN (RWO "-2<" (-1) THENA Auto)
   THEN ThinVar `b'
   THEN ListInd (-3)
   THEN Auto
   THEN Try ((BagMemberD (-1) THEN Auto))
   THEN D (-1)
   THEN (Unhide THENA Auto)
   THEN D (-1)
   THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  ((\mforall{}x,y:T.    Dec(x  =  y))  {}\mRightarrow{}  (\mforall{}L:T  List.  \mforall{}b:bag(T).  \mforall{}x:T.    ((L  =  b)  {}\mRightarrow{}  x  \mdownarrow{}\mmember{}  b  {}\mRightarrow{}  (x  \mmember{}  L))))


By

---

Latex:
((UnivCD  THENA  Auto)
  THEN  (RWO  "-2<"  (-1)  THENA  Auto)
  THEN  ThinVar  `b'
  THEN  ListInd  (-3)
  THEN  Auto
  THEN  Try  ((BagMemberD  (-1)  THEN  Auto))
  THEN  D  (-1)
  THEN  (Unhide  THENA  Auto)
  THEN  D  (-1)
  THEN  Auto)

---

Home Index