---

Step * of Lemma bsubmset_weakening

∀s:DSet. ∀a,b:MSet{s}.  ((a = b ∈ MSet{s}) ⇒ (↑(a ⊆b b)))
BY
{ ((RW mset_elimC 0) THENA Auto) }

1
∀s:DSet. ∀a,b:|s| List.  ((a ≡(|s|) b) ⇒ (↑(mk_mset(a) ⊆b mk_mset(b))))

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a,b:MSet\{s\}.    ((a  =  b)  {}\mRightarrow{}  (\muparrow{}(a  \msubseteq{}\msubb{}  b)))


By

---

Latex:
((RW  mset\_elimC  0)  THENA  Auto)

---

Home Index