---

Step * 1 of Lemma mem_iff_exists


1. s : DSet
2. a : |s|
3. bs : |s| List
⊢ ∃n:ℕ||bs||. (↑(bs[n] (=b) a)) ⇐⇒ ∃n:ℕ||bs||. (bs[n] = a ∈ |s|)
BY
{ (RW bool_to_propC 0 THEN Auto') }

---

Latex:

---

Latex:

1.  s  :  DSet
2.  a  :  |s|
3.  bs  :  |s|  List
\mvdash{}  \mexists{}n:\mBbbN{}||bs||.  (\muparrow{}(bs[n]  (=\msubb{})  a))  \mLeftarrow{}{}\mRightarrow{}  \mexists{}n:\mBbbN{}||bs||.  (bs[n]  =  a)


By

---

Latex:
(RW  bool\_to\_propC  0  THEN  Auto')

---

Home Index