proposition: Theorem reduction : SSTS01 ⪯ CD_INH.
proof: Proof. exists (fun rs => (Γ_init ++ Γ_step rs, triangle)). intros rs. split. - intros [n Hn%completeness]. destruct Hn as [N [? HN]]. exists N. exact HN. - intros [N HN]. destruct (weak_normalization HN) as [N' HN' H'N']. apply (soundness rs N'). + exact H'N'. + exact (type_preservation HN' HN). Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.StringRewriting.SSTS Undecidability.LambdaCalculus.Util.term_facts Relations List PeanoNat Lia ssreflect ssrfun Undecidability.Synthetic.Definitions Undecidability.IntersectionTypes.Util.CD_wn