proposition: Lemma normal_form_app_neutral M N : normal_form (app M N) -> neutral normal_form (app M N).
proof: Proof. by move=> > /normal_form_neutral [?|[?] [??]]. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect