proposition: Lemma s_update_f : forall r x v r', s_update r x v r' -> uf r x v = Some r'.
proof: Proof. induction 1; simpl. case (string_dec x x); intuition. case (string_dec y x); intuition. assert False ; auto; intuition. rewrite IHs_update; auto. Qed.
imports: ZArith List syntax Lia