proposition: Theorem RU2SemiU_undec : undecidable RU2SemiU.
proof: Proof. apply (undecidability_from_reducibility SSemiU_undec). exact SSemiU_to_RU2SemiU.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.SemiUnification.SemiU Undecidability.StackMachines.SSM_undec