proposition: Theorem not_decidable X Y (p : X -> Prop) (q : Y -> Prop) : p ⪯ q -> enumerable__T X -> ~ enumerable (complement p) -> ~ decidable q /\ ~ decidable (complement q).
proof: Proof. intros. split; intros ?. - eapply H1. eapply dec_red in H2; eauto. eapply dec_compl in H2. eapply dec_count_enum; eauto. - eapply H1. eapply dec_red in H2; eauto. eapply dec_count_enum; eauto. now eapply red_comp. Qed.
imports: Undecidability.Synthetic(ReducibilityFacts DecidabilityFacts EnumerabilityFacts ListEnumerabilityFacts MoreEnumerabilityFacts) List Undecidability.Shared(Dec)