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'); cbn in |- *; tauto. Qed.
imports: Relations List ZArith Arith