proposition: Theorem HSC_PRV_undec : undecidable (HSC_PRV ΓPCP).
proof: Proof. apply (undecidability_from_reducibility MPCPb_undec). exact MPCPb_to_HSC_PRV.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.HilbertCalculi.HSC Undecidability.PCP.PCP_undec