---

Step * 1 of Lemma mk_mset_cons


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}
BY
{ Assert (mset_inj{s}(a) + mk_mset(as)) = (mset_inj{s}(a) + mk_mset(as)) ∈ MSet{s} 
 }

1
.....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}

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

---

Latex:

---

Latex:

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


By

---

Latex:
Assert  (mset\_inj\{s\}(a)  +  mk\_mset(as))  =  (mset\_inj\{s\}(a)  +  mk\_mset(as)) 

---

Home Index