proposition: Theorem aeval_iff_aevalR' : forall a n, (a ==> n) <-> aeval a = n.
proof: Proof. split. - intros H; induction H; subst; reflexivity. - generalize dependent n. induction a; simpl; intros; subst; constructor; try apply IHa1; try 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)