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