---

Step * 2 of Lemma fset_of_mset_mem


1. s : DSet
2. c : |s|
⊢ c ∈b fset_of_mset(s;0{s}) = c ∈b 0{s}
BY
{ ((Unfold `fset_of_mset` 0 THEN Reduce 0) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  c  :  |s|
\mvdash{}  c  \mmember{}\msubb{}  fset\_of\_mset(s;0\{s\})  =  c  \mmember{}\msubb{}  0\{s\}


By

---

Latex:
((Unfold  `fset\_of\_mset`  0  THEN  Reduce  0)  THEN  Auto)

---

Home Index