proposition: Lemma X_gen : generating X.
proof: Proof. Proof using Hf HX. intros A. destruct (sub_dec (LX (length A)) A) as [H|H]. - apply NoDup_incl_length in H; try apply LX_NoDup. rewrite LX_len in H. lia. - destruct H as [x [_ H] ]. now exists x. Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia