---

Step * of Lemma bag-member-single-weak

∀[T:Type]. ∀[x,y:T].  (x ↓∈ {y} ⇐⇒ x = y ∈ T)
BY
{ (Auto THEN Try ((BagMemberD (-1) THEN Auto)) THEN Try ((BagMemberD (0) THEN Auto))) }

---

Latex:

---

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


By

---

Latex:
(Auto  THEN  Try  ((BagMemberD  (-1)  THEN  Auto))  THEN  Try  ((BagMemberD  (0)  THEN  Auto)))

---

Home Index