proposition: Lemma update_af'_var_subst : forall r1 x v r2 e g s, s_update r1 x v r2 -> aeval r1 e v -> af' (r2@g) (avar s) = af' (r1@g) (subst (avar s) x e).
proof: Proof. intros r1 x v r2 e g s H He; simpl subst. case (string_dec x s). intros; subst s; rewrite (af'_correct r1 e v); auto. apply update_af' with (1:= H). intros Hnxs; apply update_af'_diff with (1:= H); auto. Qed.
imports: syntax little denot Bool List String ZArith