Step
*
1
1
of Lemma
eq_mset_iff_eq_counts
.....assertion.....
1. s : DSet
2. as : |s| List
3. bs : |s| List
4. as ≡(|s|) bs
5. v : |s| List
6. v1 : |s| List
7. v ≡(|s|) v1
⊢ mk_mset(as) = mk_mset(v) ∈ MSet{s}
⇐⇒ ∀x:|s|. ((x #∈ as) = (x #∈ v) ∈ ℤ)
BY
{ ((RWH (LemmaC `equal_mset_elim`) 0) THENA Auto)⋅ }
1
1. s : DSet
2. as : |s| List
3. bs : |s| List
4. as ≡(|s|) bs
5. v : |s| List
6. v1 : |s| List
7. v ≡(|s|) v1
⊢ as ≡(|s|) v
⇐⇒ ∀x:|s|. ((x #∈ as) = (x #∈ v) ∈ ℤ)
Latex:
Latex:
.....assertion.....
1. s : DSet
2. as : |s| List
3. bs : |s| List
4. as \mequiv{}(|s|) bs
5. v : |s| List
6. v1 : |s| List
7. v \mequiv{}(|s|) v1
\mvdash{} mk\_mset(as) = mk\_mset(v) \mLeftarrow{}{}\mRightarrow{} \mforall{}x:|s|. ((x \#\mmember{} as) = (x \#\mmember{} v))
By
Latex:
((RWH (LemmaC `equal\_mset\_elim`) 0) THENA Auto)\mcdot{}
Home
Index