proposition: Lemma step'_or_nf M : (exists N, step' M N) \/ (normal_form M).
proof: Proof. by move: (step_dec M) => [[? /step_step']|/not_step_normal_form]; auto. Qed.
imports: Undecidability.IntersectionTypes.CD Undecidability.IntersectionTypes.Util.CD_facts Undecidability.LambdaCalculus.Util.term_facts PeanoNat Relations List Lia ssreflect