proposition: Lemma remove_in m x y `{!Ok m} : y ∈ remove x m <-> ~ y == x /\ y ∈ m.
proof: Proof. functional induction (remove x m); simpl; intros; cleanf; invok; rewrite ?append_in, ?bal_in, ?IHt; intuition_in; order. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)