proposition: Theorem wCBNclosed_undec : undecidable wCBNclosed.
proof: Proof. apply (undecidability_from_reducibility HaltL_undec). apply (reduces_transitive HaltL_to_HaltLclosed.reduction). exact HaltLclosed_to_wCBNclosed.reduction. Qed.
imports: Undecidability.Synthetic(Undecidability ReducibilityFacts) Undecidability.LambdaCalculus.Lambda Undecidability.L.L_undec Undecidability.LambdaCalculus.Krivine_undec