proposition: Lemma remove_spec2 m x y {Hm: Ok m} : ~K.eq x y -> find y (remove x m) = find y m.
proof: Proof. induction m as [ | (k,e') m IH]; simpl; trivial; intros E. inversion_clear Hm. repeat (dec; simpl); auto. elim E. now transitivity k. Qed.
imports: Coq(EqualitiesFacts)