proposition: Theorem set_Some : forall A x y v u dom (m : t A dom) (Hin : Dom.In x dom), find y (set x v m Hin) = 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 Hin. destruct (X.eq_dec y x) as [Hxy | Hxy]. + rewrite Hxy. rewrite set_same. split; intro Heq. - left. inversion Heq. split; reflexivity. - destruct Heq as [[_ Heq] | [Habs _]]. now subst. now elim Habs. + rewrite set_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