proposition: Lemma PCSnf_undec : undecidable PCSnf.
proof: Proof. apply (undecidability_from_reducibility SR_undec). exact SR_to_PCSnf.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.StringRewriting.PCSnf Undecidability.StringRewriting.SR_undec