proposition: Theorem aeval_free: forall s1 s2 a, (forall x, free_in_aexp x a -> s1 x = s2 x) -> aeval a s1 = aeval a s2.
proof: Proof. induction a; cbn; intros SAMEFREE. - auto. - apply SAMEFREE. auto. - rewrite IHa1, IHa2; auto. - rewrite IHa1, IHa2; auto. Qed.
imports: Coq(Arith ZArith Psatz Bool String List Program.Equality) CDF(Sequences Simulation)