proposition: Theorem gsspec: forall (A:Type)(i j: key) (x: A) (m: t A), find i (add j x m) = if E.eq_dec i j then Some x else find i m.
proof: Proof. intros. destruct (E.eq_dec i j) as [ ->|]; [ apply gss | apply gso; auto ]. Qed.
imports: Bool OrderedType ZArith OrderedType OrderedTypeEx FMapInterface