Require Import Undecidability.Synthetic.Undecidability.

Require Import Undecidability.IntersectionTypes.CD.
From Undecidability.IntersectionTypes.Reductions Require
  SSTS01_to_CD_INH CD_TYP_to_CD_TC SNclosed_to_CD_TYP.

Require Import Undecidability.StringRewriting.SSTS_undec.
Require Import Undecidability.LambdaCalculus.Lambda_undec.

Theorem CD_INH_undec : undecidable CD_INH.
Proof.
  apply (undecidability_from_reducibility SSTS01_undec).
  exact SSTS01_to_CD_INH.reduction.
Qed.

Check CD_INH_undec.

Theorem CD_TYP_undec : undecidable CD_TYP.
Proof.
  apply (undecidability_from_reducibility SNclosed_undec).
  exact SNclosed_to_CD_TYP.reduction.
Qed.

Check CD_TYP_undec.

Theorem CD_TC_undec : undecidable CD_TC.
Proof.
  apply (undecidability_from_reducibility CD_TYP_undec).
  exact CD_TYP_to_CD_TC.reduction.
Qed.

Check CD_TC_undec.