---

Step * 1 1 of Lemma mk_mset_cons

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

---

Latex:

---

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


By

---

Latex:
Auto

---

Home Index