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(Init.Nat) Coq(Arith.Arith) Coq(Arith.EqNat) Coq(Lia) Coq(Lists.List) Coq(Strings.String) LF(Maps)