proposition: Lemma bindings_Equal_eqlistA (m m' : t elt) : m == m' <-> eqlistA eqke (bindings m) (bindings m').
proof: Proof. split; intros. - apply sort_equivlistA_eqlistA; auto with *. red; intros. destruct x; do 2 rewrite <- bindings_mapsto_iff. do 2 rewrite find_mapsto_iff; rewrite H; split; auto. - unfold Equal. setoid_rewrite bindings_o. induction H; simpl; intros; auto. destruct x as (x,e), x' as (x',e'). compute in H. destruct H. subst e'. unfold eqb in *. do 2 case K.eq_dec; auto; order. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)