proposition: Theorem add_Some : forall A x y v u dom (m : t A dom), find y (add x v m) = Some u <-> X.eq y x ∧ u = v ∨ ¬X.eq y x ∧ find y m = Some u.
proof: Proof. intros A x y v u dom m. destruct (X.eq_dec y x) as [Hxy | Hxy]. + rewrite Hxy. rewrite add_same. split; intro Heq. - left. inversion Heq. split; reflexivity. - destruct Heq as [[_ Heq] | [Habs _]]. now subst. now elim Habs. + rewrite add_other; trivial. split; intro Heq. - right. split; assumption. - destruct Heq as [[Habs _] | [_ Heq]]. contradiction. assumption. Qed.
imports: Utf8 Bool SetoidList RelationPairs Orders Coqlib DepMapInterface DepMapFactsInterface