proposition: Lemma constant_OK_aux : forall A v (m : S.t A) l x, S.In x (fold_left (λ (a : S.t A) (e : Dom.elt), S.add e v a) l m) <-> S.In x m ∨ InA X.eq x l.
proof: Proof. intros A v m l x. revert m. induction l as [| y l]; intro m; simpl. * rewrite InA_nil. intuition. * split; intro Hin. + destruct (X.eq_dec x y) as [Hxy | Hxy]. - right; left. assumption. - rewrite IHl in Hin. destruct Hin as [[v' Hin] | Hin]. left. exists v'. apply S.add_3 in Hin; auto. now symmetry. now do 2 right. + rewrite IHl. destruct Hin as [Hin | Hin]. - left. destruct (X.eq_dec x y) as [Hxy | Hxy]. exists v. apply S.add_1. now auto. destruct Hin as [v' Hin]. exists v'. apply S.add_2; auto. now symmetry. - inversion_clear Hin. left. exists v. apply S.add_1. now auto. now right. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface