proposition: Lemma bf_eval : forall r e v, bf r e = Some v -> beval r e v.
proof: Proof. Proof with eauto with zarith. intros r (e1,e2) v;simpl. case_eq (af r e1); case_eq (af r e2); try (intros; discriminate). intros v1 Heq1 v2 Heq2; unfold bind. generalize (Zlt_cases v2 v1); destruct (Zlt_bool v2 v1); intros comp Heq; injection Heq; intros; subst v... Qed.
imports: ZArith List syntax Lia