---

Step * of Lemma assert-deq-member

∀[A:Type]. ∀eq:EqDecider(A). ∀L:A List. ∀x:A.  (↑x ∈b L ⇐⇒ (x ∈ L))
BY
{ (InductionOnList THEN Try (Reduce 0)) }

1
1. [A] : Type
2. eq : EqDecider(A)
⊢ ∀x:A. (False ⇐⇒ (x ∈ []))

2
1. [A] : Type
2. eq : EqDecider(A)
3. u : A
4. v : A List
5. ∀x:A. (↑x ∈b v ⇐⇒ (x ∈ v))
⊢ ∀x:A. (↑((eq u x) ∨bx ∈b v) ⇐⇒ (x ∈ [u / v]))

---

Latex:

---

Latex:
\mforall{}[A:Type].  \mforall{}eq:EqDecider(A).  \mforall{}L:A  List.  \mforall{}x:A.    (\muparrow{}x  \mmember{}\msubb{}  L  \mLeftarrow{}{}\mRightarrow{}  (x  \mmember{}  L))


By

---

Latex:
(InductionOnList  THEN  Try  (Reduce  0))

---

Home Index