---

Step * 1 of Lemma bsubmset_weakening


∀s:DSet. ∀a,b:|s| List.  ((a ≡(|s|) b) ⇒ (↑(mk_mset(a) ⊆b mk_mset(b))))
BY
{ ((RepD THENM All (RWW "bsubmset_elim") 
THENM RelRST) THEN Auto) }

---

Latex:

---

Latex:

\mforall{}s:DSet.  \mforall{}a,b:|s|  List.    ((a  \mequiv{}(|s|)  b)  {}\mRightarrow{}  (\muparrow{}(mk\_mset(a)  \msubseteq{}\msubb{}  mk\_mset(b))))


By

---

Latex:
((RepD  THENM  All  (RWW  "bsubmset\_elim") 
THENM  RelRST)  THEN  Auto)

---

Home Index