proposition: Lemma neutralE P M : neutral P M -> match M with | var _ => True | app M N => neutral P M /\ P N | lam _ => False end.
proof: Proof. by case. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect