proposition: Theorem not_coenumerable X Y (p : X -> Prop) (q : Y -> Prop) : p ⪯ q -> enumerable__T X -> ~ enumerable (complement p) -> discrete Y -> ~ enumerable (complement q).
proof: Proof. intros. intros ?. eapply H1. eapply enumerable_red in H3; eauto. now eapply red_comp. Qed.
imports: Undecidability.Synthetic(ReducibilityFacts DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts MoreEnumerabilityFacts) List Undecidability.Shared(Dec)