proposition: Lemma del_spec2 m x y `{!Ok m} : ~ x == y -> find y (del x m) = find y m.
proof: Proof. intros. apply find_mapsto_equiv; ok. induct m. - easy. - rewrite append_mapsto, node_mapsto. treeorder. - destmatch. + simpl. intuition_m. + rewrite 2 node_mapsto. factornode l. now rewrite IHl by ok. + rewrite lbalS_mapsto, 2 node_mapsto. factornode l. now rewrite IHl by ok. - destmatch. + simpl. intuition_m. + rewrite 2 node_mapsto. factornode r. now rewrite IHr by ok. + rewrite rbalS_mapsto, 2 node_mapsto. factornode r. now rewrite IHr by ok. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)