proposition: Lemma Equivb_bindings m m' : Equivb eqb m m' <-> L.Equivb eqb (bindings m) (bindings m').
proof: Proof. unfold Equivb, L.Equivb; split; split; try red; intros. do 2 rewrite bindings_in; firstorder. destruct H. apply (H2 k); rewrite <- bindings_spec1; auto. do 2 rewrite <- bindings_in; firstorder. destruct H. apply (H2 k); unfold L.PX.MapsTo; rewrite bindings_spec1; auto. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)