From Undecidability.L Require Import L.



Definition HaltL s := exists t, eval s t.
Definition HaltLclosed (s : {s : term | closed s}) := exists t, eval (proj1_sig s) t.