proposition: Lemma update_f_p_subst : forall r1 x v r2 e' m g s l, s_update r1 x v r2 -> aeval r1 e' v -> (f_p m s (lf' (r1@g) (l_subst l x e')) <-> f_p m s (lf' (r2@g) l)).
proof: Proof. intros r1 x v r2 e' m g s l Hu He'; induction m. simpl; intros; split; auto. destruct a as [p1 P]; simpl; case (string_dec p1 s). rewrite update_lf'_subst with (1:= Hu) (2:= He'). intros; split; auto. intros; apply IHm. Qed.
imports: syntax little denot Bool List String ZArith