proposition: Lemma step_many_app s t ts : step s t -> step (many_app s ts) (many_app t ts).
proof: Proof. elim /rev_ind: ts. { done. } move=> ?? IH /= ?. rewrite !fold_left_app /=. by auto using step with nocore. Qed.
imports: Undecidability.LambdaCalculus(Lambda Krivine Util.term_facts Util.wCBN_facts Util.Krivine_facts) List Relations ssreflect