proposition: Lemma neutral_normal_form M : neutral normal_form M -> normal_form M.
proof: Proof. elim. - by constructor. - move=> > []; do ? constructor; by auto. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect