proposition: Lemma aeval_f : forall r e n, aeval r e n -> af r e = Some n.
proof: Proof. induction 1; simpl; auto. destruct (string_dec x x); intuition. destruct (string_dec y x); auto. elim H; auto. rewrite IHaeval1; simpl; rewrite IHaeval2; simpl; auto. Qed.
imports: ZArith List syntax Lia