proposition: Lemma LL_F x n : x el LL n -> exists m, F m = x.
proof: Proof. induction n; cbn; [easy|]. intros [H|[H|H]] % in_app_iff; [auto| |easy]. now exists n. Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia