---

Step * 1 of Lemma mset_map_char


1. s : DSet
2. s' : DSet
3. f : |s| ⟶ |s'|
⊢ msmap{s,s'}(f;mk_mset([])) = mk_mset([]) ∈ MSet{s'}
BY
{ % This is ugly % 
Assert msmap{s,s'}(f;0{s}) = 0{s'} ∈ MSet{s'} 
THENM (Unfold `mk_mset` 0 THEN Unfold `null_mset` (-1) 
       THEN Trivial) }

1
.....assertion..... 
1. s : DSet
2. s' : DSet
3. f : |s| ⟶ |s'|
⊢ msmap{s,s'}(f;0{s}) = 0{s'} ∈ MSet{s'}

---

Latex:

---

Latex:

1.  s  :  DSet
2.  s'  :  DSet
3.  f  :  |s|  {}\mrightarrow{}  |s'|
\mvdash{}  msmap\{s,s'\}(f;mk\_mset([]))  =  mk\_mset([])


By

---

Latex:
\%  This  is  ugly  \% 
Assert  msmap\{s,s'\}(f;0\{s\})  =  0\{s'\} 
THENM  (Unfold  `mk\_mset`  0  THEN  Unfold  `null\_mset`  (-1) 
              THEN  Trivial)

---

Home Index