---

Step * 1 of Lemma mset_mon_for_elim


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}
BY
{ ListInd 4 THEN AbReduce 0 }

1
1. s : DSet
2. T : Type
3. f : T ⟶ (|s| List)
⊢ 0{s} = mk_mset([]) ∈ MSet{s}

2
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}

---

Latex:

---

Latex:

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


By

---

Latex:
ListInd  4  THEN  AbReduce  0

---

Home Index