---

Step * of Lemma bsubmset_wf

∀s:DSet. ∀a,b:MSet{s}.  (a ⊆b b ∈ 𝔹)
BY
{ (((Unfold `bsubmset` 0 THEN RepD) THENA Auto)
   THEN (OnVar `a' msetD THENA Auto) 
        THENM (OnVar `b' msetD THENA Auto)⋅
   ) }

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
⊢ bsublist(s;as;v) = bsublist(s;bs;v1)

---

Latex:

---

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


By

---

Latex:
(((Unfold  `bsubmset`  0  THEN  RepD)  THENA  Auto)
  THEN  (OnVar  `a'  msetD  THENA  Auto) 
            THENM  (OnVar  `b'  msetD  THENA  Auto)\mcdot{}
  )

---

Home Index