---

Step * of Lemma member_exists

∀[T:Type]. ∀L:T List. ∃x:T. (x ∈ L) supposing ¬(L = [] ∈ (T List))
BY
{ ((((Unfold `l_member` 0 THEN Auto) THEN AssertBY 0 < ||L|| (D 2 THEN Auto' THEN D -1 THEN Auto))
    THEN InstConcl [L[0];0]
    )
   THEN Auto
   ) }

---

Latex:

---

Latex:
\mforall{}[T:Type].  \mforall{}L:T  List.  \mexists{}x:T.  (x  \mmember{}  L)  supposing  \mneg{}(L  =  [])


By

---

Latex:
((((Unfold  `l\_member`  0  THEN  Auto)  THEN  AssertBY  0  <  ||L||  (D  2  THEN  Auto'  THEN  D  -1  THEN  Auto))
    THEN  InstConcl  [L[0];0]
    )
  THEN  Auto
  )

---

Home Index