proposition: Lemma update_af'_subst : forall r1 x v r2 e' g e, s_update r1 x v r2 -> aeval r1 e' v -> af' (r2@g) e = af' (r1@g) (subst e x e').
proof: Proof. intros r1 x v r2 e' g e Hup He'; induction e. apply update_af'_var_subst with (1:= Hup); auto. trivial. simpl; rewrite IHe1; rewrite IHe2; auto. Qed.
imports: syntax little denot Bool List String ZArith