proposition: Lemma HaltUTM_undec : undecidable HaltUTM.
proof: Proof. apply (undecidability_from_reducibility KrivineMclosed_HALT_undec). exact KrivineMclosed_HALT_to_HaltUTM.reduction. Qed.
imports: Undecidability(Synthetic.Undecidability Synthetic.ReducibilityFacts LambdaCalculus.Krivine_undec TM.UTM)