proposition: Lemma bindings_b : forall m x, mem x m = existsb (fun p => eqb x (fst p)) (bindings m).
proof: Proof. intros. apply eq_bool_alt. rewrite mem_spec, bindings_in_iff, existsb_exists. split. - intros (e,H). rewrite InA_alt in H. destruct H as ((k,e'),((H1,H2),H')); simpl in *; subst e'. exists (k, e); split; trivial. simpl. now apply eqb_eq. - intros ((k,e),(H,H')); simpl in *. apply eqb_eq in H'. exists e. rewrite InA_alt. exists (k,e). now repeat split. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)