---

Step * of Lemma mset_mon_for_elim

∀s:DSet. ∀T:Type. ∀f:T ⟶ (|s| List). ∀as:T List.
  ((For{mset_mon{s}} x ∈ as. mk_mset(f[x])) = mk_mset(For{<s List, @>} x ∈ as. f[x]) ∈ MSet{s})
BY
{ ((UnivCD) THENA Auto) }

1
1. s : DSet
2. T : Type
3. f : T ⟶ (|s| List)
4. as : T List
⊢ (For{mset_mon{s}} x ∈ as. mk_mset(f[x])) = mk_mset(For{<s List, @>} x ∈ as. f[x]) ∈ MSet{s}

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}T:Type.  \mforall{}f:T  {}\mrightarrow{}  (|s|  List).  \mforall{}as:T  List.
    ((For\{mset\_mon\{s\}\}  x  \mmember{}  as.  mk\_mset(f[x]))  =  mk\_mset(For\{<s  List,  @>\}  x  \mmember{}  as.  f[x]))


By

---

Latex:
((UnivCD)  THENA  Auto)

---

Home Index