proposition: Lemma listable_enumerable X : listable X -> enumerable__T X.
proof: Proof. intros [L HL]. exists (nth_error L). intros x. apply In_nth_error, HL. Qed.
imports: Undecidability.FOL.Semantics(Tarski.FragmentFacts) Undecidability.FOL.Syntax(Facts) Undecidability.Synthetic.DecidabilityFacts Undecidability.Synthetic.EnumerabilityFacts Undecidability.Shared.Dec List