proposition: Lemma F_sur : forall x, exists n, F n = x.
proof: Proof. intros x. destruct (f_sur x) as [n H]. destruct (LL_F (LL_f n)) as [m H']. exists m. congruence. Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia