---

Step * of Lemma mem_iff_mem_f

∀s:DSet. ∀a:|s|. ∀bs:|s| List.  (↑(a ∈b bs) ⇐⇒ mem_f(|s|;a;bs))
BY
{ (InductionOnListA THEN Reduce 0 THEN Try ((RW bool_to_propC 0 THENM RWH (HypC 5) 0)) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}s:DSet.  \mforall{}a:|s|.  \mforall{}bs:|s|  List.    (\muparrow{}(a  \mmember{}\msubb{}  bs)  \mLeftarrow{}{}\mRightarrow{}  mem\_f(|s|;a;bs))


By

---

Latex:
(InductionOnListA  THEN  Reduce  0  THEN  Try  ((RW  bool\_to\_propC  0  THENM  RWH  (HypC  5)  0))  THEN  Auto)

---

Home Index