---

Step * of Lemma member-exists2

∀[T:Type]. ∀L:T List. (∃x:T. (x ∈ L) ⇐⇒ 0 < ||L||)
BY
{ ((UnivCD THENM RWO "member-exists" 0 THENM RWO "length_of_not_nil" 0) THEN Auto) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  (\mexists{}x:T.  (x  \mmember{}  L)  \mLeftarrow{}{}\mRightarrow{}  0  <  ||L||)


By

---

Latex:
((UnivCD  THENM  RWO  "member-exists"  0  THENM  RWO  "length\_of\_not\_nil"  0)  THEN  Auto)

---

Home Index