proposition: Lemma step_bound s k t : step s t -> bound k s -> bound k t.
proof: Proof. elim. - move=> > /boundE [/boundE /bound_subst +] ?. apply. move=> [|n] /=; first done. move=> ?. constructor. lia. - move=> > ? ? /boundE [? ?]. constructor; by auto with nocore. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts) Undecidability.L.Util.L_facts Relations Lia ssreflect