---

Step * of Lemma eq_mset_iff_eq_counts

∀s:DSet. ∀a,b:MSet{s}.  (a = b ∈ MSet{s} ⇐⇒ ∀x:|s|. ((x #∈ a) = (x #∈ b) ∈ ℤ))
BY
{ (((RepD  
   THENM CSquash 
   THENM UseEqWitness Ax) THENA Auto)
   THEN ((OnVar `a' msetD) THENA Auto)⋅
   THEN ((OnVar `b' msetD) THENA Auto)⋅
   THEN MemTypeCD) }

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 = v ∈ MSet{s} ⇐⇒ ∀x:|s|. ((x #∈ as) = (x #∈ v) ∈ ℤ)

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a,b:MSet\{s\}.    (a  =  b  \mLeftarrow{}{}\mRightarrow{}  \mforall{}x:|s|.  ((x  \#\mmember{}  a)  =  (x  \#\mmember{}  b)))


By

---

Latex:
(((RepD   
  THENM  CSquash 
  THENM  UseEqWitness  Ax)  THENA  Auto)
  THEN  ((OnVar  `a'  msetD)  THENA  Auto)\mcdot{}
  THEN  ((OnVar  `b'  msetD)  THENA  Auto)\mcdot{}
  THEN  MemTypeCD)

---

Home Index