proposition: Lemma LX_len n : length (LX n) = S n.
proof: Proof. Proof using Hf. induction n; cbn; eauto. Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia