proposition: Lemma undecidability_from_complement {X} {p : X -> Prop} : undecidable (complement p) -> undecidable p.
proof: Proof. intros H Hp. now apply H, dec_compl. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.Synthetic.DecidabilityFacts Undecidability.Synthetic.ReducibilityFacts Undecidability.TM.SBTM