Require Import Undecidability.CFG.CFG.
From Undecidability.CFG.Reductions Require
CFPP_to_CFP CFPI_to_CFI.
Require Import Undecidability.Synthetic.Undecidability.
Require Undecidability.CFG.CFP_undec.
Lemma CFP_undec : undecidable CFP.
Proof.
eapply undecidability_from_reducibility.
exact CFP_undec.CFPP_undec.
exact CFPP_to_CFP.reduction.
Qed.
Check CFP_undec.
Lemma CFI_undec : undecidable CFI.
Proof.
eapply undecidability_from_reducibility.
exact CFP_undec.CFPI_undec.
exact CFPI_to_CFI.reduction.
Qed.
Check CFI_undec.
From Undecidability.CFG.Reductions Require
CFPP_to_CFP CFPI_to_CFI.
Require Import Undecidability.Synthetic.Undecidability.
Require Undecidability.CFG.CFP_undec.
Lemma CFP_undec : undecidable CFP.
Proof.
eapply undecidability_from_reducibility.
exact CFP_undec.CFPP_undec.
exact CFPP_to_CFP.reduction.
Qed.
Check CFP_undec.
Lemma CFI_undec : undecidable CFI.
Proof.
eapply undecidability_from_reducibility.
exact CFP_undec.CFPI_undec.
exact CFPI_to_CFI.reduction.
Qed.
Check CFI_undec.