proposition: Lemma neutral_dec P M : (forall M, P M \/ not (P M)) -> neutral P M \/ not (neutral P M).
proof: Proof. move=> H. elim: M. - left. by constructor. - move=> M []. + move=> ? N _. case: (H N). * left. by constructor. * move=> ?. by right => /neutralE []. + move=> *. by right => /neutralE []. - by right=> /neutralE. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect