Step * of Lemma member_exists

[T:Type]. ∀L:T List. ∃x:T. (x ∈ L) supposing ¬(L [] ∈ (T List))
BY
((((Unfold `l_member` THEN Auto) THEN AssertBY 0 < ||L|| (D THEN Auto' THEN -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