proposition: Lemma LX_NoDup n : NoDup (LX n).
proof: Proof. Proof using Hf. induction n; cbn; repeat constructor; auto. intros (n'&H1&H2) % LX_el. apply Hf in H2. lia. Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia