---

Step * 3 of Lemma fset_of_mset_mem


1. s : DSet
2. c : |s|
⊢ ∀x:|s|. c ∈b fset_of_mset(s;mset_inj{s}(x)) = c ∈b mset_inj{s}(x)
BY
{ ((Unfold `fset_of_mset` 0 
THENM RWH (LemmaC `mset_mem_char`) 0 
THENM RW mset_for_normC 0) THENA Auto)  }

1
1. s : DSet
2. c : |s|
⊢ ∀x:|s|. x (=b) c = x (=b) c

---

Latex:

---

Latex:

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


By

---

Latex:
((Unfold  `fset\_of\_mset`  0 
THENM  RWH  (LemmaC  `mset\_mem\_char`)  0 
THENM  RW  mset\_for\_normC  0)  THENA  Auto) 

---

Home Index