proposition: Lemma enumerable_enumerable_T X : enumerable (fun _ : X => True) <-> enumerable__T X.
proof: Proof. split. - intros [e He]. exists e. intros x. now eapply He. - intros [c Hc]. exists c. intros x. split; eauto. Qed.
imports: Undecidability.Synthetic(DecidabilityFacts SemiDecidabilityFacts) Undecidability.Shared.Libs.PSL.FiniteTypes.FinTypesDef Vector List Lia