---

Step * of Lemma comb_for_mod_mssum_wf

λs,r,m,f,a,z. Σm x ∈ a. f[x] ∈ s:DSet ⟶ r:Rng ⟶ m:r-Module ⟶ f:(|s| ⟶ m.car) ⟶ a:MSet{s} ⟶ (↓True) ⟶ m.car
BY
{ ProveOpCombTyping `mod_mssum_wf` }

---

Latex:

---

Latex:
\mlambda{}s,r,m,f,a,z.  \mSigma{}m  x  \mmember{}  a.  f[x]  \mmember{}  s:DSet
{}\mrightarrow{}  r:Rng
{}\mrightarrow{}  m:r-Module
{}\mrightarrow{}  f:(|s|  {}\mrightarrow{}  m.car)
{}\mrightarrow{}  a:MSet\{s\}
{}\mrightarrow{}  (\mdownarrow{}True)
{}\mrightarrow{}  m.car


By

---

Latex:
ProveOpCombTyping  `mod\_mssum\_wf`

---

Home Index