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 _ _ (, n) M tp)
             ( (@ext _ _ _ (term_test (mk_mconfig (start M) tp))))).
  intros [ [ n] M tp ]. cbn. eapply Halt_red.
Qed.

Print Assumptions Halt_eva.