---

Step * 1 of Lemma mem_bsublist


1. s : DSet
2. as : DisList{s}
3. bs : |s| List
4. ↑bsublist(s;as;bs)
5. c : |s|
6. ↑(c ∈b as)
⊢ ↑(c ∈b bs)
BY
{ (Using [`as',as] (BLemma `mem_bsublist_imp`) THEN Auto) }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  as  :  DisList\{s\}
3.  bs  :  |s|  List
4.  \muparrow{}bsublist(s;as;bs)
5.  c  :  |s|
6.  \muparrow{}(c  \mmember{}\msubb{}  as)
\mvdash{}  \muparrow{}(c  \mmember{}\msubb{}  bs)


By

---

Latex:
(Using  [`as',as]  (BLemma  `mem\_bsublist\_imp`)  THEN  Auto)

---

Home Index