proposition: Lemma elements_b : forall m x, mem x m = existsb (fun p => eqb x (fst p)) (elements m).
proof: Proof. intros. generalize (mem_in_iff m x)(elements_in_iff m x) (existsb_exists (fun p => eqb x (fst p)) (elements m)). destruct (mem x m); destruct (existsb (fun p => eqb x (fst p)) (elements m)); auto; intros. - symmetry; rewrite H1. destruct H0 as (H0,_). destruct H0 as (e,He); [ intuition |]. rewrite InA_alt in He. destruct He as ((y,e'),(Ha1,Ha2)). compute in Ha1; destruct Ha1; subst e'. exists (y,e); split; simpl; auto. unfold eqb; destruct (eq_dec x y); intuition. - rewrite <- H; rewrite H0. destruct H1 as (H1,_). destruct H1 as ((y,e),(Ha1,Ha2)); [intuition|]. simpl in Ha2. unfold eqb in *; destruct (eq_dec x y); auto; try discriminate. exists e; rewrite InA_alt. exists (y,e); intuition. compute; auto. Qed.
imports: Bool DecidableType DecidableTypeEx OrderedType Morphisms FMapInterface