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