proposition: Lemma bindings_spec1 m k e : InA eq_key_elt (k,e) (bindings m) <-> MapsTo k e m.
proof: Proof. unfold bindings, MapsTo. rewrite xbindings_spec. split; [ intros [H|(y & H & H')] | intros IN ]. - inversion H. - simpl in *. now subst. - right. now exists k. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)