proposition: Lemma to_enumerator__T {X} (f : t -> option X) : (forall x, exists r, f r = Some x) -> enumerator__T (fun n => f (of_nat n)) X.
proof: Proof. intros Hf x. destruct (Hf x) as [r Hr]. exists (to_nat r). now rewrite cancel_of_to. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia