proposition: Lemma add_spec2 m x y e `{!Ok m} : ~ x == y -> find y (add x e m) = find y m.
proof: Proof. functional induction (add x e m); simpl; intros; cleanf; trivial. - case K.compare_spec; trivial; order. - case K.compare_spec; trivial; order. - invok. rewrite bal_find by autok. simpl. now rewrite IHt0. - invok. rewrite bal_find by autok. simpl. now rewrite IHt0. Qed.
imports: Coq(Bool PeanoNat BinInt FunInd Int) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)