proposition: Lemma remove_spec1 m x `{!Ok m} : find x (remove x m) = None.
proof: Proof. intros. apply not_find_iff; autok. rewrite remove_in; intuition (auto with map). Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)