proposition: Lemma update_other: forall x v s y, x <> y -> (update x v s) y = s y.
proof: Proof. unfold update; intros. destruct (string_dec x y); congruence. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)