proposition: Remark diff_key2 : forall (d:dict) (k k':key) (v v':data), k <> k' -> occ v k (D_tree d) -> occ v k (D_tree (add k' v' d)).
proof: Proof. simple destruct d; cbn in |- *; intros x s k k' v v'; case (insert k' v' x s); cbn in |- *; simple destruct 1; intros H H0 H1 H2 H3 H4; case (H _ _ H4). - intro H5; case (H3 H5); auto. - auto. Qed.
imports: Relations List ZArith Arith