---

Step * of Lemma eq_mset_wf

∀s:DSet. ∀a,b:MSet{s}.  (eq_mset{s}(a,b) ∈ 𝔹)
BY
{ ((UnivCD) THENA Auto) 
THEN Unfolds ``eq_mset member`` 0 }

1
1. s : DSet@i'
2. a : MSet{s}@i
3. b : MSet{s}@i
⊢ a ≡b b = a ≡b b

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a,b:MSet\{s\}.    (eq\_mset\{s\}(a,b)  \mmember{}  \mBbbB{})


By

---

Latex:
((UnivCD)  THENA  Auto) 
THEN  Unfolds  ``eq\_mset  member``  0

---

Home Index