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. intros. case (occ_dec k (D_tree d)). apply D_search. simple destruct 1. intros x Hx. transitivity (Some x). apply find_occ_dec. apply diff_key2; auto. symmetry in |- *; apply find_occ_dec; auto. intro; transitivity (None (A:=data)). apply not_find_occ_dec. intros v0 H0. apply (n v0). eapply diff_key1; eauto. symmetry in |- *; apply not_find_occ_dec. auto. Qed.
imports: Relations List ZArith Arith