From Undecidability.Synthetic Require Import Undecidability ReducibilityFacts.

Require Import Undecidability.LambdaCalculus.wCBN.
From Undecidability.LambdaCalculus.Reductions Require
  HaltLclosed_to_wCBNclosed wCBNclosed_to_wCBN.

Require Import Undecidability.L.L_undec.
Require Undecidability.L.Reductions.HaltL_to_HaltLclosed.

Theorem wCBNclosed_undec : undecidable wCBNclosed.
Proof.
  apply (undecidability_from_reducibility HaltL_undec).
  apply (reduces_transitive HaltL_to_HaltLclosed.reduction).
  exact HaltLclosed_to_wCBNclosed.reduction.
Qed.

Check wCBNclosed_undec.

Theorem wCBN_undec : undecidable wCBN.
Proof.
  apply (undecidability_from_reducibility wCBNclosed_undec).
  exact wCBNclosed_to_wCBN.reduction.
Qed.

Check wCBN_undec.