proposition: Lemma step_dec M : (exists N, step M N) \/ (forall N, not (step M N)).
proof: Proof. elim: M. - move=> ?. by right=> ? /stepE. - move=> M [[M' IH1]|IH1]. { move=> ? _. left. eexists. apply: stepAppL. by eassumption. } move=> N [[N' IH2]|IH2]. { left. eexists. apply: stepAppR. by eassumption. } case: M IH1. + move=> > IH1. by right=> ? /stepE [|[|]] [?] [] => [|/IH1|/IH2]. + move=> > IH1. by right=> ? /stepE [|[|]] [?] [] => [|/IH1|/IH2]. + move=> *. left. eexists. by apply: stepSubst. - move=> M [[??]|IH]. + left. eexists. apply: stepLam. by eassumption. + by right=> ? /stepE [?] [/IH]. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect