include "basics/lists/listb.ma".
include "ASM/Util.ma".

lemma Exists_memb : ∀S:DeqSet. ∀x:S. ∀l:list S.
  Exists S (λy. y = x) l →
  x ∈ l.
#S #x #l elim l 
[ //
| #h #t #IH
  normalize lapply (eqb_true … x h)
  cases (x==h) *
  [ #E #_ >(E (refl ??)) //
  | #_ #E * [ #E' destruct lapply (E (refl ??)) #E'' destruct
            | #H @IH @H
            ]
  ]
] qed.