proposition: Lemma form_enumerable : enumerable__T form.
proof: Proof. Proof using enumerable_quantop enumerable_preds enumerable_funcs enumerable_binop. apply enum_enumT. apply enum_enumT in enumerable_funcs as [Lf HLf]. apply enum_enumT in enumerable_preds as [Lp HLp]. apply enum_enumT in enumerable_binop as [Lb HLb]. apply enum_enumT in enumerable_quantop as [Lq HLq]. eexists. apply enum_form. Qed.
imports: Undecidability.SOL.SOL Undecidability.Shared.Dec Undecidability.Shared.Libs.PSL(Vectors) Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) EqdepFacts Eqdep_dec List