proposition: Lemma CFPI_undec : undecidable CFPI.
proof: Proof. eapply undecidability_from_reducibility. exact PCP_undec.PCP_undec. exact PCP_to_CFPI.reduction. Qed.
imports: Undecidability.CFG.CFP Undecidability.Synthetic.Undecidability