proposition: Lemma gen_le_f A : forall x, ~ x el A -> le_f (gen' A) x.
proof: Proof. unfold gen'. destruct (gen A); cbn. apply a. Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia