proposition: Lemma update_lf'_subst : forall r1 x v r2 e' g l, s_update r1 x v r2 -> aeval r1 e' v -> lf' (r2@g) l = lf' (r1@g) (l_subst l x e').
proof: Proof. intros r1 x v r2 e' g l Hu He'; induction l. simpl; auto. simpl; rewrite update_af'_subst with (1:= Hu)(2:= He'). rewrite IHl; auto. Qed.
imports: syntax little denot Bool List String ZArith