proposition: Theorem add_spec2: forall (m: t A) (i j: key) (x: A), i <> j -> find j (add i x m) = find j m.
proof: Proof. intros m i j; revert m i. induction j; destruct i, m; simpl; intros; rewrite ?IHj, ?gleaf; auto; try congruence. Qed.
imports: Coq(Bool PeanoNat BinPos Orders OrdersEx OrdersLists) MMaps(Utils Comparisons Interface)