---

Step * of Lemma mk_mset_cons

∀s:DSet. ∀a:|s|. ∀as:|s| List.  (mk_mset([a / as]) = (mset_inj{s}(a) + mk_mset(as)) ∈ MSet{s})
BY
{ ((RepD) THENA Auto) }

1
1. s : DSet@i'
2. a : |s|@i
3. as : |s| List@i
⊢ mk_mset([a / as]) = (mset_inj{s}(a) + mk_mset(as)) ∈ MSet{s}

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a:|s|.  \mforall{}as:|s|  List.    (mk\_mset([a  /  as])  =  (mset\_inj\{s\}(a)  +  mk\_mset(as)))


By

---

Latex:
((RepD)  THENA  Auto)

---

Home Index