proposition: Lemma beval_f : forall r e b, beval r e b -> bf r e = Some b.
proof: Proof. induction 1; simpl; rewrite aeval_f with (1:= H); rewrite aeval_f with (1:= H0);simpl; generalize (Zlt_cases v1 v2); case (Zlt_bool v1 v2); auto; intros H'; assert False by lia; contradiction. Qed.
imports: ZArith List syntax Lia