---

Step * of Lemma decidable__bag-member

∀[T:Type]. ((∀x,y:T.  Dec(x = y ∈ T)) ⇒ (∀x:T. ∀bs:bag(T).  Dec(x ↓∈ bs)))
BY
{ (Auto
   THEN FLemma `deq-exists` [2]
   THEN Auto
   THEN RenameVar `eq' (-1)
   THEN (InstLemma `bag-member-count` [⌜T⌝;⌜eq⌝]⋅ THENA Auto)
   THEN RWO  "-1" 0
   THEN Auto) }

---

Latex:

---

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


By

---

Latex:
(Auto
  THEN  FLemma  `deq-exists`  [2]
  THEN  Auto
  THEN  RenameVar  `eq'  (-1)
  THEN  (InstLemma  `bag-member-count`  [\mkleeneopen{}T\mkleeneclose{};\mkleeneopen{}eq\mkleeneclose{}]\mcdot{}  THENA  Auto)
  THEN  RWO    "-1"  0
  THEN  Auto)

---

Home Index