proposition: Lemma ins_in m x v y : y ∈ (ins x v m) <-> y == x \/ y ∈ m.
proof: Proof. induct m; destmatch; autorew; rewrite ?IHl, ?IHr; intuition_in. setoid_replace y with x; eauto. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)