proposition: Lemma remove_spec1 m x {Hm: Ok m} : find x (remove x m) = None.
proof: Proof. induction m as [ | (k,e') m IH]; simpl; trivial. inversion_clear Hm. repeat (dec; simpl); auto. destruct (find x m) eqn:F; trivial. apply find_spec in F; trivial. elim H. apply InA_eqk with (x,e); auto. Qed.
imports: Coq(EqualitiesFacts)