proposition: Lemma stepE {s t} : step s t -> match s with | app (lam s') t' => stepLam_spec s' t' t | app s' t' => stepApp_spec s' t' t | _ => False end.
proof: Proof. by elim; [|case]. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts) Undecidability.L.Util.L_facts Relations Lia ssreflect