proposition: Lemma normal_form_not_step {M} : normal_form M -> forall N, not (step M N).
proof: Proof. elim. - by move=> > /stepE. - by move=> > _ IH ? /stepE [?] [/IH]. - move=> > ? IH ? /stepE. by move=> [|[|]] [?] [] => [|/stepE|/IH]. - move=> > _ IH1 _ IH2 ? /stepE. by move=> [|[|]] [?] [] => [|/IH1|/IH2]. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect