proposition: Theorem remove_compat : forall A x y dom₁ dom₂ (m₁ : t A dom₁) (m₂ : t A dom₂), X.eq x y -> eq m₁ m₂ -> eq (remove x m₁) (remove y m₂).
proof: Proof. intros ? x y * Hxy Heq z. destruct (X.eq_dec z x) as [Hxz | Hxz]. + rewrite Hxz. rewrite Hxy at 4. do 2 rewrite remove_same. reflexivity. + repeat rewrite remove_other. apply Heq. now rewrite <- Hxy. assumption. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface