proposition: Lemma ins_arb x e s n : rbt n s -> arbt n (ins x e s).
proof: Proof. intros H. apply (ins_rr_rb x e), ifred_or in H. intuition (auto with map). Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList Arith) Coq(Orders OrdersFacts OrdersLists) MMaps(Interface GenTree RBT)