Require Import TM.TMEncoding TM.TM.
Require Import MuRec.
Require Import Undecidability.FOL.Reductions.

Turing machine halting reduces to L halting

Theorem Halt_eva :
  Halt ⪯ converges.
Proof.
  eexists (fun '(existT2 _ _ (Sigma, n) M tp) =>
             (mu (@ext _ _ _ (term_test (mk_mconfig (start M) tp))))).
  intros [ [Sigma n] M tp ]. cbn. eapply Halt_red.
Qed.

Print Assumptions Halt_eva.