proposition: Lemma step_closed s t : step s t -> closed s -> closed t.
proof: Proof. by move=> /step_bound + /closed_dcl => /[apply] /closed_dcl. Qed.
imports: Undecidability.LambdaCalculus(Lambda Util.term_facts) Undecidability.L.Util.L_facts Relations Lia ssreflect