proposition: Theorem LU2SemiU_undec : undecidable LU2SemiU.
proof: Proof. apply (undecidability_from_reducibility RU2SemiU_undec). exact RU2SemiU_to_LU2SemiU.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.SemiUnification.SemiU Undecidability.StackMachines.SSM_undec