proposition: Lemma step'_step M N : step' M N -> step M N.
proof: Proof. case. - elim; by auto using step. - elim; [|by auto using step..]. move=> > _. apply: stepSubst'. by rewrite !simpl_term. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect