proposition: Theorem wn_step'_sn_step (M N : term) : steps' M N -> normal_form N -> sn M.
proof: Proof. move=> /clos_rt_rt1n_iff HMN HN. suff: typable M. { move=> [] >. by apply: CD_sn.strong_normalization. } elim: HMN HN. - by apply: nf_typable. - move=> > /subject_expansion. by auto. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect