proposition: Lemma Sdom_aux : forall A x (m : S.t A) s, Dom.In x (S.fold (fun x _ acc => Dom.add x acc) m s) <-> S.In x m ∨ Dom.In x s.
proof: Proof. intros A x m. setoid_rewrite S.fold_1. assert (Hequiv : S.In x m ↔ (∃ v : A, InA (X.eq * eq)%signature (x, v) (S.elements m))). { split; intros [v Hin]; exists v; apply S.elements_1 + apply S.elements_2; assumption. } setoid_rewrite Hequiv. generalize (S.elements m). intro l. induction l as [| [x' v'] l]; simpl. * setoid_rewrite InA_nil. firstorder. * intro s. rewrite IHl. clear IHl. rewrite Dom.add_spec. split; intros [[v Hin] | Hin]. + left. exists v. right. assumption. + destruct Hin as [Heq |Hin]. - left. exists v'. left. split; trivial. reflexivity. - tauto. + inversion_clear Hin. - destruct H. tauto. - left. exists v. assumption. + tauto. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface