proposition: Lemma normal_form_neutral M : normal_form M -> neutral normal_form M \/ (exists N, M = lam N /\ normal_form N).
proof: Proof. elim. - move=> >. left. by constructor. - move=> *. right. by do ? econstructor. - move=> *. left. by do ? constructor. - move=> > ? [?| [? [??]]]; [|done]. left. by constructor. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect