proposition: Lemma undecidability_from_reducibility {X} {p : X -> Prop} {Y} {q : Y -> Prop} : undecidable p -> p ⪯ q -> undecidable q.
proof: Proof. unfold undecidable, decidable, decider, reduces, reduction, reflects. intros H [f Hf] [d Hd]. eapply H. exists (fun x => d (f x)). intros x. rewrite Hf. eapply Hd. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.DecidabilityFacts Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.SBTM