proposition: Lemma LX_el n x : x el LX n -> exists n', n' <= n /\ f n' = x.
proof: Proof. induction n. - intros [H|[] ]. exists 0. split; auto. - intros [H|H]; eauto. destruct (IHn H) as [n'[H1 H2] ]. exists n'. split; auto. Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia