proposition: Theorem KrivineM_HALT_undec : undecidable KrivineM_HALT.
proof: Proof. apply (undecidability_from_reducibility KrivineMclosed_HALT_undec). exists (@proj1_sig L.term _). now intros [??]. Qed.
imports: Undecidability.Synthetic(Undecidability ReducibilityFacts) Undecidability.LambdaCalculus.Krivine Undecidability.L.L_undec