proposition: Lemma bindings_Eqdom_eqlistA (m m' : t elt) : Eqdom m m' <-> eqlistA eqk (bindings m) (bindings m').
proof: Proof. split; intros. - apply SortA_equivlistA_eqlistA with (ltA:=ltk); eauto with *. intros (k,e). now rewrite <- !in_bindings_iff'. - unfold Eqdom. setoid_rewrite bindings_in_iff. induction H; simpl; auto. + now setoid_rewrite InA_nil. + intros y. setoid_rewrite InA_cons. destruct x as (x,e), x' as (x',e'). compute in H. split; intros (e2,[E|IN]); try (firstorder; fail); compute in E; destruct E; subst; eexists; left; compute; split; eauto; order. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)