---

Step * of Lemma mset_for_inj_lemma

∀f,a,y,g,s:Top.  (msFor{g} x ∈ mset_inj{s}(y) + a. f[x] ~ f[y] * (msFor{g} x ∈ a. f[x]))
BY
{ (UnivCD THENA Auto) }

1
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])

---

Latex:

---

Latex:
\mforall{}f,a,y,g,s:Top.    (msFor\{g\}  x  \mmember{}  mset\_inj\{s\}(y)  +  a.  f[x]  \msim{}  f[y]  *  (msFor\{g\}  x  \mmember{}  a.  f[x]))


By

---

Latex:
(UnivCD  THENA  Auto)

---

Home Index