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