proposition: Lemma constant_aux : forall A v x u l (m : S.t A), NoDupA X.eq l -> S.find x (fold_left (fun a e => S.add e v a) l m) = Some u <-> InA X.eq x l ∧ u = v ∨ ¬InA X.eq x l ∧ S.find x m = Some u.
proof: Proof. intros A v x u l. induction l as [| x' l]; intros m Hl; simpl. * rewrite InA_nil. tauto. * rewrite IHl. clear IHl. split; intro Hin. + destruct Hin as [[Hin ?] | [? Hin]]. - left. split; trivial. now right. - { destruct (X.eq_dec x' x) as [Heq | Heq]. + left. rewrite Heq. split; try now left. cut (Some u = Some v). intro Heq'; inversion Heq'; reflexivity. rewrite <- Hin. apply S.find_1. eapply S.MapsTo_1, S.add_1; try eassumption || reflexivity. + right. split. - intro Habs. inversion_clear Habs; solve [contradiction | apply Heq; symmetry; assumption]. - eapply S.find_1, S.add_3, S.find_2; eassumption. } + destruct Hin as [[Hin ?] | [? Hin]]. - subst. inversion_clear Hin; try tauto. right. split. inversion_clear Hl. rewrite H. assumption. apply S.find_1, S.add_1. symmetry; assumption. - right. split. intro Habs. apply H. now right. apply S.find_1, S.add_2, S.find_2; trivial. intro Habs. apply H. now left. + inversion_clear Hl. assumption. Qed.
imports: Utf8 MSets FMaps Orders Coqlib DepMapInterface