proposition: Lemma enumerator_enumerable {X} {f} : enumerator__T f X -> enumerable__T X.
proof: Proof. intros H. exists f. eapply H. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia