proposition: Lemma gen (A : list X) : { x | ~ x el A /\ forall y, ~ y el A -> le_f x y}.
proof: Proof. Proof using HX. pose (p := fun n => ~ f n el A). assert (H1 : forall x, dec (p x)). { intros n. destruct (el_dec A (f n)) as [H|H]. - right. intros H'. contradiction. - left. assumption. } assert (H2 : exists x, p x). { destruct (Hg A) as [x Hx]. destruct (f_sur x) as [n <-]. now exists n. } exists (f (mu' H1 H2)). split; try apply proj2_sig. intros y Hy. exists (mu' H1 H2). split; trivial. intros n <-. apply mu_least, Hy. Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia