proposition: Lemma find_in_equiv m m' x `{!Ok m, !Ok m'} : find x m = find x m' -> (x ∈ m <-> x ∈ m').
proof: Proof. intros E. split; intros; apply find_in; [ rewrite <- E | rewrite E ]; apply in_find; auto. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)