proposition: Lemma cbv_steps_closed {s s'} : clos_refl_trans cbv_step s s' -> closed s -> closed s'.
proof: Proof. elim; by eauto using cbv_step_closed. 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)