---

Step * of Lemma rng_mssum_elim_lemma

∀[s,r,as,f:Top].  (Σx ∈ mk_mset(as). f[x] ~ Σ{r} x ∈ as. f[x])
BY
{ (RepUR ``mk_mset rng_mssum mset_for rng_lsum mon_for for tlambda`` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[s,r,as,f:Top].    (\mSigma{}x  \mmember{}  mk\_mset(as).  f[x]  \msim{}  \mSigma{}\{r\}  x  \mmember{}  as.  f[x])


By

---

Latex:
(RepUR  ``mk\_mset  rng\_mssum  mset\_for  rng\_lsum  mon\_for  for  tlambda``  0  THEN  Auto)

---

Home Index