From Undecidability.Synthetic Require Import Undecidability ReducibilityFacts.

Require Import Undecidability.LambdaCalculus.Krivine.
From Undecidability.LambdaCalculus.Reductions Require
  wCBNclosed_to_KrivineMclosed_HALT
  HaltLclosed_to_wCBNclosed.
Require Undecidability.L.Reductions.HaltL_to_HaltLclosed.

Require Import Undecidability.L.L_undec.

Theorem KrivineMclosed_HALT_undec : undecidable KrivineMclosed_HALT.
Proof.
  apply (undecidability_from_reducibility HaltL_undec).
  apply (reduces_transitive HaltL_to_HaltLclosed.reduction).
  apply (reduces_transitive HaltLclosed_to_wCBNclosed.reduction).
  exact wCBNclosed_to_KrivineMclosed_HALT.reduction.
Qed.

Check KrivineMclosed_HALT_undec.

Theorem KrivineM_HALT_undec : undecidable KrivineM_HALT.
Proof.
  apply (undecidability_from_reducibility KrivineMclosed_HALT_undec).
  exists (@proj1_sig L.term _). now intros [??].
Qed.

Check KrivineM_HALT_undec.