proposition: Lemma CFI_undec : undecidable CFI.
proof: Proof. eapply undecidability_from_reducibility. exact CFP_undec.CFPI_undec. exact CFPI_to_CFI.reduction. Qed.
imports: Undecidability.CFG.CFG Undecidability.Synthetic.Undecidability