proposition: Lemma stepE M N : step M N -> match M with | var _ => False | app M1 M2 => (exists M3, M1 = lam M3 /\ N = (subst (scons M2 var) M3)) \/ (exists M1', step M1 M1' /\ N = app M1' M2) \/ (exists M2', step M2 M2' /\ N = app M1 M2') | lam M => exists M', step M M' /\ N = lam M' end.
proof: Proof. case=> *. - left. by eexists. - right. left. eexists. by split; [eassumption|]. - right. right. eexists. by split; [eassumption|]. - eexists. by split; [eassumption|]. Qed.
imports: Undecidability.LambdaCalculus.Lambda PeanoNat Lia List Relations ssreflect