proposition: Theorem CD_INH_undec : undecidable CD_INH.
proof: Proof. apply (undecidability_from_reducibility SSTS01_undec). exact SSTS01_to_CD_INH.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.IntersectionTypes.CD Undecidability.StringRewriting.SSTS_undec Undecidability.LambdaCalculus.Lambda_undec