proposition: Remark diff_key1 : forall (d:dict) (k k':key) (v v':data), k <> k' -> occ v k (D_tree (add k' v' d)) -> occ v k (D_tree 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 (H1 _ _ H4); auto. simple destruct 1; absurd (k' = k); auto. tauto. Qed.
imports: Relations List ZArith Arith