proposition: Lemma add_in m x v y : y ∈ (add x v m) <-> y == x \/ y ∈ m.
proof: Proof. unfold add. now autorew. Qed.
imports: Coq(Bool BinPos Pnat Setoid SetoidList PeanoNat) Coq(Orders OrdersFacts OrdersLists) MMaps(Utils Interface OrdList GenTree)