proposition: Theorem SNclosed_undec : undecidable SNclosed.
proof: Proof. apply (undecidability_from_reducibility KrivineMclosed_HALT_undec). exact KrivineMclosed_HALT_to_SNclosed.reduction. Qed.
imports: Undecidability.Synthetic(Undecidability ReducibilityFacts) Undecidability.LambdaCalculus.Lambda Undecidability.L.L_undec Undecidability.LambdaCalculus.Krivine_undec