---

Step * 1 2 of Lemma mk_mset_cons


1. s : DSet@i'
2. a : |s|@i
3. as : |s| List@i
4. (mset_inj{s}(a) + mk_mset(as)) = (mset_inj{s}(a) + mk_mset(as)) ∈ MSet{s}
⊢ mk_mset([a / as]) = (mset_inj{s}(a) + mk_mset(as)) ∈ MSet{s}
BY
{ OnCls [0;4] (Eval ``mset_inj mk_mset mset_sum``) 
THEN Trivial }

---

Latex:

---

Latex:

1.  s  :  DSet@i'
2.  a  :  |s|@i
3.  as  :  |s|  List@i
4.  (mset\_inj\{s\}(a)  +  mk\_mset(as))  =  (mset\_inj\{s\}(a)  +  mk\_mset(as))
\mvdash{}  mk\_mset([a  /  as])  =  (mset\_inj\{s\}(a)  +  mk\_mset(as))


By

---

Latex:
OnCls  [0;4]  (Eval  ``mset\_inj  mk\_mset  mset\_sum``) 
THEN  Trivial

---

Home Index