---

Step * of Lemma mset_mem_inj_sum_lemma

∀a,y,x,s:Top.  (x ∈b mset_inj{s}(y) + a ~ (y (=b) x) ∨b(x ∈b a))
BY
{ ((UnivCD THENA Auto) THEN RepUR ``mset_inj mk_mset mset_sum mset_mem`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}a,y,x,s:Top.    (x  \mmember{}\msubb{}  mset\_inj\{s\}(y)  +  a  \msim{}  (y  (=\msubb{})  x)  \mvee{}\msubb{}(x  \mmember{}\msubb{}  a))


By

---

Latex:
((UnivCD  THENA  Auto)  THEN  RepUR  ``mset\_inj  mk\_mset  mset\_sum  mset\_mem``  0  THEN  Auto)

---

Home Index