proposition: Theorem SSemiU_undec : undecidable SSemiU.
proof: Proof. apply (undecidability_from_reducibility CSSM_UB_undec). exact CSSM_UB_to_SSemiU.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.SemiUnification.SemiU Undecidability.StackMachines.SSM_undec