---

Step * 1 of Lemma fset_of_mset_mem


1. s : DSet
2. c : |s|
⊢ ∀w:MSet{s}. SqStable(c ∈b fset_of_mset(s;w) = c ∈b w)
BY
{ Auto }

---

Latex:

---

Latex:

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


By

---

Latex:
Auto

---

Home Index