proposition: Lemma bindings_o : forall m x, find x m = findA (eqb x) (bindings m).
proof: Proof. intros. rewrite eq_option_alt. intro e. rewrite <- find_mapsto_iff, bindings_mapsto_iff. unfold eqb. rewrite <- findA_NoDupA; dintuition auto; try apply bindings_3w; eauto with map. Qed.
imports: Coq(Bool Equalities Orders OrdersFacts OrdersLists) Coq(Morphisms Permutation SetoidPermutation) MMaps(Utils Comparisons Interface)