proposition: Lemma enumerator__T_nat : enumerator__T nat_enum nat.
proof: Proof. intros n. now eexists. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia