proposition: Lemma a_subst_correct : forall a r1 e v m g r2 x, aeval r1 e v -> s_update r1 x v r2 -> (i_a m (r1@g) (a_subst a x e)<-> i_a m (r2@g) a).
proof: Proof. induction a; simpl; intros r1 e v m g r2 x H Hu. destruct b as [e1 e2]; unfold bf', b_subst. repeat rewrite update_af'_subst with (1:= Hu) (2:=H); split; auto. split; intros H1 Habs; case H1; elim (IHa r1 e v m g r2 x H Hu); auto. split; intros [H1 H2]; (split; [elim (IHa1 r1 e v m g r2 x H Hu)| elim (IHa2 r1 e v m g r2 x H Hu)]); auto. apply update_f_p_subst with (1:=Hu)(2:=H). Qed.
imports: syntax little denot Bool List String ZArith