proposition: Lemma CFP_undec : undecidable CFP.
proof: Proof. eapply undecidability_from_reducibility. exact CFP_undec.CFPP_undec. exact CFPP_to_CFP.reduction. Qed.
imports: Undecidability.CFG.CFG Undecidability.Synthetic.Undecidability