proposition: Lemma agree'_update_dead: forall s1 s2 L x v, agree' L s1 s2 -> ~IdentSet.In x L -> agree' L (update x v s1) s2.
proof: Proof. unfold agree', update; intros. destruct (string_dec x x0). - subst x0. contradiction. - apply H. fsetdec. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)