proposition: Lemma bindings_in m x : L.PX.In x (bindings m) <-> x ∈ m.
proof: Proof. unfold L.PX.In. split; intros (y,H); exists y. - now rewrite <- bindings_spec1. - unfold L.PX.MapsTo; now rewrite bindings_spec1. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)