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