proposition: Lemma mapsto_eq {elt} m x y (e:elt) : x == y -> m@x ↦ e -> m@y ↦ e.
proof: Proof. induction m; simpl; intuition_m; eauto. constructor. F.order. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)