proposition: Lemma to_enumerable_T X : (exists (f : t -> option X), forall x, exists r, f r = Some x) -> enumerable__T X.
proof: Proof. intros [f Hf]. eexists. apply to_enumerator__T. eassumption. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia