proposition: Lemma step_wn M N : step M N -> wn N -> wn M.
proof: Proof. move=> ? [???]. econstructor; [|eassumption]. by apply: rt_trans; [apply: rt_step|]; eassumption. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.IntersectionTypes.Util.CD_fundamental Undecidability.LambdaCalculus.Util.term_facts Relations ssreflect