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); try reflexivity. - destruct a1; try (simpl; simpl in IHa1; rewrite IHa1; rewrite IHa2; reflexivity). + destruct n; simpl; rewrite IHa2; reflexivity. Qed.
imports: Coq.Bool.Bool Coq.Arith.Arith Coq.Arith.EqNat Coq.omega.Omega Coq.Lists.List Coq.omega.Omega Maps