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