proposition: Lemma add_spec2' m x y e : ~K.eq x y -> find y (add x e m) = find y m.
proof: Proof. intros N. assert (N' : ~K.eq y x) by now contradict N. induction m as [ | (k,e') m IH]; simpl. - dec; trivial. - repeat (dec; simpl); trivial. elim N. now transitivity k. Qed.
imports: Coq(EqualitiesFacts)