---

Step * 1 of Lemma mset_for_inj_lemma


1. f : Top
2. a : Top
3. y : Top
4. g : Top
5. s : Top
⊢ msFor{g} x ∈ mset_inj{s}(y) + a
    f[x] ~ f[y] * (msFor{g} x ∈ a. f[x])
BY
{ (RepUR ``mset_inj mk_mset mset_sum mset_for`` 0⋅ THEN Auto) }

---

Latex:

---

Latex:

1.  f  :  Top
2.  a  :  Top
3.  y  :  Top
4.  g  :  Top
5.  s  :  Top
\mvdash{}  msFor\{g\}  x  \mmember{}  mset\_inj\{s\}(y)  +  a
        f[x]  \msim{}  f[y]  *  (msFor\{g\}  x  \mmember{}  a.  f[x])


By

---

Latex:
(RepUR  ``mset\_inj  mk\_mset  mset\_sum  mset\_for``  0\mcdot{}  THEN  Auto)

---

Home Index