proposition: Lemma neutral_impl (P Q : term -> Prop) M : (forall N, P N -> Q N) -> neutral P M -> neutral Q M.
proof: Proof. move=> H. elim; by auto using neutral. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect