proposition: Theorem remove_Some : forall A x y u dom (m : t A dom), find y (remove x m) = Some u <-> ¬X.eq y x ∧ find y m = Some u.
proof: Proof. intros A x y u dom m. destruct (X.eq_dec y x) as [Hxy | Hxy]. + rewrite Hxy, remove_same. split; intro Hin. - discriminate Hin. - destruct Hin as [Hin _]. now elim Hin. + rewrite remove_other; trivial. intuition. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface