proposition: Lemma af_eval : forall r e v, af r e = Some v -> aeval r e v.
proof: Proof. Proof with eauto. induction e; intros v... simpl; intros Heq; injection Heq; intros; subst... simpl; case_eq (af r e2); case_eq (af r e1); try (intros;discriminate). intros v1 Heq1 v2 Heq2 Heq; injection Heq; intros; subst... Qed.
imports: ZArith List syntax Lia