proposition: Theorem success : forall (d : dict) (k : key) (v : data), find k (add k v d) = Some v.
proof: Proof. unfold find, add in |- *; intros d k v. case (Key.eqdec k k); simpl in |- *; tauto. Qed.
imports: Relations List ZArith Arith