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 d k k' v H; 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