---

Step * 1 2 of Lemma mset_mon_for_elim


1. s : DSet
2. T : Type
3. f : T ⟶ (|s| List)
4. u : T
5. v : T List
6. (For{mset_mon{s}} x ∈ v. mk_mset(f[x])) = mk_mset(For{<s List, @>} x ∈ v. f[x]) ∈ MSet{s}
⊢ (mk_mset(f[u]) + (For{mset_mon{s}} x ∈ v. mk_mset(f[x]))) = mk_mset(f[u] @ (For{<s List, @>} x ∈ v. f[x])) ∈ MSet{s}
BY
{ (((RWH (HypC (-1)) 0) THENA Auto) THEN RWH mset_sum_elimC 0 THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  T  :  Type
3.  f  :  T  {}\mrightarrow{}  (|s|  List)
4.  u  :  T
5.  v  :  T  List
6.  (For\{mset\_mon\{s\}\}  x  \mmember{}  v.  mk\_mset(f[x]))  =  mk\_mset(For\{<s  List,  @>\}  x  \mmember{}  v.  f[x])
\mvdash{}  (mk\_mset(f[u])  +  (For\{mset\_mon\{s\}\}  x  \mmember{}  v.  mk\_mset(f[x])))
=  mk\_mset(f[u]  @  (For\{<s  List,  @>\}  x  \mmember{}  v.  f[x]))


By

---

Latex:
(((RWH  (HypC  (-1))  0)  THENA  Auto)  THEN  RWH  mset\_sum\_elimC  0  THEN  Auto)

---

Home Index