proposition: Lemma remove_spec2 m x y `{!Ok m} : ~ x == y -> find y (remove x m) = find y m.
proof: Proof. functional induction (remove x m); simpl; intros; cleanf; invok; autok. - case K.compare_spec; intros; try order; rewrite find_mapsto_equiv; eauto using append_ok, between; intros; rewrite append_mapsto; intuition; order. - rewrite bal_find by autok. simpl. case K.compare_spec; auto. - rewrite bal_find by autok. simpl. case K.compare_spec; auto. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)