proposition: Lemma agree'_update_move: forall s1 s2 L x y, agree' (IdentSet.union (IdentSet.remove x L) (IdentSet.singleton y)) s1 s2 -> (forall z, IdentSet.In z L -> z <> x -> z <> y -> f z <> f x) -> agree' L (update x (s1 y) s1) (update (f x) (s2 (f y)) s2).
proof: Proof. unfold agree', update; intros. destruct (string_dec x x0); destruct (string_dec (f x) (f x0)). - apply H. fsetdec. - congruence. - destruct (string_dec x0 y). + subst x0. apply H. fsetdec. + exfalso. apply (H0 x0); auto. - apply H. fsetdec. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)