proposition: Theorem optimize_0plus_sound': forall a, aeval (optimize_0plus a) = aeval a.
proof: Proof. intros a. induction a; try (simpl; rewrite IHa1; rewrite IHa2; reflexivity). - reflexivity. - destruct a1 eqn:Ea1; try (simpl; simpl in IHa1; rewrite IHa1; rewrite IHa2; reflexivity). + destruct n eqn:En; simpl; rewrite 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)