proposition: Lemma in_impl_mem : (forall a, eqA a a) -> forall e l, In e l -> mem e l.
proof: Proof. intros refl_eq e l e_in_l; rewrite (mem_in_eq e l); exists e; split; [apply (refl_eq e) | assumption]. Qed.
imports: Coq(Bool List Arith Setoid Relations FunInd) CoLoR(closure)