proposition: Lemma PA2_form_enumerable : enumerable__T form.
proof: Proof. apply form_enumerable. - apply list_enumerable__T_enumerable. exists L_PA2_funcs. apply PA2_funcs_enum. - apply list_enumerable__T_enumerable. exists L_PA2_preds. apply PA2_preds_enum. - apply enumT_binop. - apply enumT_quantop. Qed.
imports: PeanoNat Lia Vector Undecidability.SOL(SOL PA2) Undecidability.Shared.Libs.PSL(Vectors) Undecidability.SOL.Util(Syntax Subst Tarski) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability.Shared.Dec