proposition: Lemma enumerable_red X Y (p : X -> Prop) (q : Y -> Prop) : p ⪯ q -> enumerable__T X -> discrete Y -> enumerable q -> enumerable p.
proof: Proof. intros [f] [] % enum_enumT [] % discrete_iff [L] % enumerable_enum. eapply list_enumerable_enumerable. eexists. eapply enum_red; eauto. Qed.
imports: Undecidability.Synthetic(ReducibilityFacts DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts MoreEnumerabilityFacts) List Undecidability.Shared(Dec)