---

Step * 1 of Lemma mset_fact


1. s : DSet
⊢ ∀a:MSet{s}. (a = (msFor{mset_mon{s}} x ∈ a. mset_inj{s}(x)) ∈ MSet{s})
BY
{ RW mset_elimC 0 THENA Auto }

1
1. s : DSet
⊢ ∀a:|s| List. (a ≡(|s|) (For{<s List, @>} x ∈ a. [x]))

---

Latex:

---

Latex:

1.  s  :  DSet
\mvdash{}  \mforall{}a:MSet\{s\}.  (a  =  (msFor\{mset\_mon\{s\}\}  x  \mmember{}  a.  mset\_inj\{s\}(x)))


By

---

Latex:
RW  mset\_elimC  0  THENA  Auto

---

Home Index