proposition: Theorem remove_cancel : forall A x dom (m : t A dom), find x m = None -> eq (remove x m) m.
proof: Proof. intros A x dom m Heq y. destruct (X.eq_dec y x) as [Hxy | Hxy]. + rewrite Hxy, remove_same, Heq. reflexivity. + rewrite remove_other; trivial. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface