proposition: Lemma find_mapsto_equiv m m' x `{!Ok m, !Ok m'} : find x m = find x m' <-> (forall d, m@x ↦ d <-> m'@x ↦ d).
proof: Proof. rewrite eq_option_alt. split; intros H d. now rewrite <- 2 find_spec. now rewrite 2 find_spec. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)