proposition: Lemma update_af' : forall x v r1 r2 g, s_update r1 x v r2 -> af' (r2@g) (avar x) = v.
proof: Proof. intros x v r1 r2 g H; induction H. simpl; case (string_dec x x); auto. intros Habs; case Habs; auto. simpl; case (string_dec y x). intros Hxy. assert (Hnxy : x<> y) by assumption; case Hnxy; auto. intros _; simpl in IHs_update; apply IHs_update. Qed.
imports: syntax little denot Bool List String ZArith