proposition: Lemma beval_agree': forall b s1 s2, agree' (fv_bexp b) s1 s2 -> beval b s1 = beval (rename_bexp b) s2.
proof: Proof. induction b; cbn; intros. - auto. - auto. - f_equal; eapply aeval_agree'; eapply agree'_mon; eauto; fsetdec. - f_equal; eapply aeval_agree'; eapply agree'_mon; eauto; fsetdec. - f_equal; apply IHb; auto. - f_equal; [apply IHb1 | apply IHb2]; eapply agree'_mon; eauto; fsetdec. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)