proposition: Lemma terminating_Acc s t : clos_refl_trans step s (lam t) -> Acc (fun t' s' => step s' t') s.
proof: Proof. move Et': (lam t) => t' /(clos_rt_rt1n term) Hst'. elim: Hst' t Et'. { move=> ?? <-. by constructor => ? /stepE. } move=> x y z Hxy Hyz IH t ?. constructor => y'. move: Hxy => /step_fun /[apply] <-. apply: IH. by eassumption. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts Util.wCBN_facts) Undecidability(L.Util.L_facts) Coq(Relations Wellfounded.Transitive_Closure List Lia) Coq(ssreflect)