proposition: Lemma gen_spec A : ~ gen' A el A.
proof: Proof. unfold gen'. destruct (gen A); cbn. apply a. Qed.
imports: Undecidability(Shared.Dec) Undecidability.Synthetic(ListEnumerabilityFacts) List PeanoNat ConstructiveEpsilon Lia