proposition: Lemma aeval_agree': forall a s1 s2, agree' (fv_aexp a) s1 s2 -> aeval a s1 = aeval (rename_aexp a) s2.
proof: Proof. induction a; cbn; intros. - auto. - apply H. fsetdec. - f_equal; [apply IHa1 | apply IHa2]; eapply agree'_mon; eauto; fsetdec. - f_equal; [apply IHa1 | apply IHa2]; eapply agree'_mon; eauto; fsetdec. Qed.
imports: Coq(ZArith Psatz Bool String Program.Equality FSets Wellfounded) CDF(Sequences IMP Simulation)