proposition: Theorem surj_form_ {ff:falsity_flag} (base : form): { Φ : nat -> form & forall y, exists x, Φ x = y }.
proof: Proof. Proof using enum_Funcs' enum_Preds' enum_binop' enum_quantop' list_Funcs list_Preds list_binop list_quantop. eexists (fun (n:nat) => match (match Cantor.of_nat n with (nn,m) => nth_error (L_form nn) m end) with Some k => k | None => base end). intros y. pose proof (list_enumerator_to_enumerator _ L_form y) as He. pose proof (enum_form y) as Hy. apply He in Hy. destruct Hy as [n Hn]. exists n. rewrite Hn. easy. Qed.
imports: Undecidability.Synthetic(Definitions DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts ReducibilityFacts) Undecidability(Shared.ListAutomation Shared.Dec) Coq(Eqdep_dec) Coq.Vectors.Vector Undecidability.Shared.Libs.PSL.Vectors(Vectors) EqdepFacts