---

Step * of Lemma l_member_decidable

∀[T:Type]. ∀x:T. ∀l:T List.  ((∀y:T. Dec(x = y ∈ T)) ⇒ Dec((x ∈ l)))
BY
{ ((InductionOnList THEN Auto) THEN RWO "nil_member cons_member" 0 THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}x:T.  \mforall{}l:T  List.    ((\mforall{}y:T.  Dec(x  =  y))  {}\mRightarrow{}  Dec((x  \mmember{}  l)))


By

---

Latex:
((InductionOnList  THEN  Auto)  THEN  RWO  "nil\_member  cons\_member"  0  THEN  Auto)

---

Home Index