proposition: Lemma find_compat m x x' `{!Ok m} : x == x' -> find x m = find x' m.
proof: Proof. intros E. destruct (find x' m) eqn:H. - apply find_1; trivial. rewrite E. now apply find_2. - rewrite not_find_iff in *; trivial. now rewrite E. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)