proposition: Lemma ins_spec1 m x v `{!Ok m} : find x (ins x v m) = Some v.
proof: Proof. induct m; simpl; destmatch; rewrite ?lbal_find, ?rbal_find by eauto with *; simpl; destmatch; auto; try order. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)