proposition: Theorem gsident: forall (A:Type)(i: key) (m: t A) (v: A), find i m = Some v -> add i v m = m.
proof: Proof. induction i; intros; destruct m; simpl; simpl in H; try congruence. - rewrite (IHi m2 v H); congruence. - rewrite (IHi m1 v H); congruence. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface