proposition: Theorem CD_TC_undec : undecidable CD_TC.
proof: Proof. apply (undecidability_from_reducibility CD_TYP_undec). exact CD_TYP_to_CD_TC.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.IntersectionTypes.CD Undecidability.StringRewriting.SSTS_undec Undecidability.LambdaCalculus.Lambda_undec