proposition: Theorem reduction : SNclosed ⪯ CD_TYP.
proof: Proof. exists (fun '(exist _ M _) => M). move=> [t Ht] /=. split. - move=> ?. by apply: sn_type_assignment. - move=> [?] [?]. by apply: CD_sn.strong_normalization. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect Undecidability.Synthetic.Definitions