---

Step * of Lemma mem_wf

∀s:DSet. ∀a:|s|. ∀bs:|s| List.  (a ∈b bs ∈ 𝔹)
BY
{ (Unfold `mem` 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a:|s|.  \mforall{}bs:|s|  List.    (a  \mmember{}\msubb{}  bs  \mmember{}  \mBbbB{})


By

---

Latex:
(Unfold  `mem`  0  THEN  Auto)

---

Home Index