proposition: Lemma find_spec m x e `{!Ok m} : find x m = Some e <-> m@x ↦ e.
proof: Proof. split; auto using find_1, find_2. Qed.
imports: Coq(Bool Arith BinInt FunInd) Coq(Orders OrdersFacts OrdersLists) MMaps(Comparisons Interface OrdList)