proposition: Theorem gso: forall (i j: key) (x: A) (m: t A), i <> j -> find i (add j x m) = find i m.
proof: Proof. induction i; intros; destruct j; destruct m; simpl; try rewrite <- (gleaf i); auto; try apply IHi; congruence. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface