proposition: Lemma closed_eval {s t} : L.eval s t -> closed s -> closed t.
proof: Proof. by move=> /eval_iff [/closed_star]. 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)