---

Step * 1 1 of Lemma mset_map_char

.....assertion..... 
1. s : DSet
2. s' : DSet
3. f : |s| ⟶ |s'|
⊢ msmap{s,s'}(f;0{s}) = 0{s'} ∈ MSet{s'}
BY
{ ((Unfold `mset_map` 0  
THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:
.....assertion..... 
1.  s  :  DSet
2.  s'  :  DSet
3.  f  :  |s|  {}\mrightarrow{}  |s'|
\mvdash{}  msmap\{s,s'\}(f;0\{s\})  =  0\{s'\}


By

---

Latex:
((Unfold  `mset\_map`  0   
THEN  Reduce  0)  THEN  Auto)

---

Home Index