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