---

Step * 1 1 1 of Lemma equal_mset_elim


1. s : DSet@i'
2. as : |s| List@i
3. bs : |s| List@i
⊢ ↑eq_mset{s}(as,bs) ⇐⇒ as = bs ∈ MSet{s}
BY
{ (((Sel (-1) (BLemma `assert_of_eq_mset`)) THEN Auto) THEN Unfold `mset` 0 THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet@i'
2.  as  :  |s|  List@i
3.  bs  :  |s|  List@i
\mvdash{}  \muparrow{}eq\_mset\{s\}(as,bs)  \mLeftarrow{}{}\mRightarrow{}  as  =  bs


By

---

Latex:
(((Sel  (-1)  (BLemma  `assert\_of\_eq\_mset`))  THEN  Auto)  THEN  Unfold  `mset`  0  THEN  Auto)

---

Home Index