proposition: Lemma SR_undec : undecidable SR.
proof: Proof. apply (undecidability_from_reducibility SBTM_HALT_undec). exact SBTM_HALT_to_SR.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.StringRewriting.SR Undecidability.TM.SBTM_undec