proposition: Theorem reduction_PCPb_HaltL : PCPb ⪯ HaltL.
proof: Proof. eapply L_recognisable_HaltL. exists sdec_PCPb. split. - econstructor. exact _. - eapply semi_decidable_PCPb. Qed.
imports: Undecidability.Synthetic(Definitions EnumerabilityFacts ListEnumerabilityFacts) Lia Undecidability.L(LProd LBool LNat LOptions) Undecidability.L.Datatypes.List(List_basics List_eqb List_extra List_nat) Undecidability(PCP) Undecidability.L(Synthetic)