proposition: Lemma clos_t_rt s t : clos_trans step s t -> clos_refl_trans step s t.
proof: Proof. elim; eauto using @clos_refl_trans. 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)