proposition: Lemma uf_s : forall r x v r', uf r x v = Some r' -> s_update r x v r'.
proof: Proof. Proof with eauto. induction r. simpl; intros; discriminate. destruct a as (y,n); simpl; intros x v r'. case (string_dec y x). intros Heq1 Heq2; injection Heq2; intros; subst; auto. case_eq (uf r x v); try(intros; discriminate). intros r'' Heqr'' Hn Heq; injection Heq; intros; subst r'; auto. Qed.
imports: ZArith List syntax Lia