proposition: Lemma steps_bound k {s t} : steps s t -> bound k s -> bound k t.
proof: Proof. elim; by eauto using step_bound. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts) Undecidability.L.Util.L_facts Relations Lia ssreflect