proposition: Lemma mem_eq : forall A (cmp:A->A->bool) x l, is_beq cmp -> mem cmp x l = isTrue (LibList.mem x l).
proof: Proof. Proof using. introv M. induction l as [|y l']; simpl; rew_listx; rew_isTrue; fequals. Qed.
imports: TLC(LibTactics LibReflect)