proposition: Theorem aeval_iff_aevalR : forall a n, (a \\ n) <-> aeval a = n.
proof: Proof. split. - intros H. induction H; simpl. + reflexivity. + rewrite IHaevalR1. rewrite IHaevalR2. reflexivity. + rewrite IHaevalR1. rewrite IHaevalR2. reflexivity. + rewrite IHaevalR1. rewrite IHaevalR2. reflexivity. - generalize dependent n. induction a; simpl; intros; subst. + apply E_ANum. + apply E_APlus. apply IHa1. reflexivity. apply IHa2. reflexivity. + apply E_AMinus. apply IHa1. reflexivity. apply IHa2. reflexivity. + apply E_AMult. apply IHa1. reflexivity. apply IHa2. reflexivity. Qed.
imports: Coq.Bool.Bool Coq.Arith.Arith Coq.Arith.EqNat Coq.omega.Omega Coq.Lists.List Coq.omega.Omega Maps