proposition: Lemma reduction : HaltL ⪯ HaltLclosed.
proof: Proof. unshelve eexists. - intros s. exists (Eval (enc s)). unfold Eval. Lproc. - cbn. intros s. unfold HaltL. split; intros (t & Ht). + eapply eval_converges. edestruct Eval_converges. eapply H. eapply eval_iff in Ht. eauto. + setoid_rewrite eval_iff. eapply eval_converges. eapply Eval_converges. eapply Seval.eval_converges. eauto. Qed.
imports: Undecidability.Synthetic.Definitions Undecidability.L(L Functions.Eval Util.L_facts)