proposition: Theorem KrivineMclosed_HALT_undec : undecidable KrivineMclosed_HALT.
proof: 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.
imports: Undecidability.Synthetic(Undecidability ReducibilityFacts) Undecidability.LambdaCalculus.Krivine Undecidability.L.L_undec