proposition: Theorem IMSELL_undec (S : IMSELL_sig3) : undecidable (@IMSELL_cf_PROVABILITY3 S).
proof: Proof. apply (undecidability_from_reducibility ndMM2_undec). now apply ndMM2_IMSELL.reduction. Qed.
imports: Undecidability.Synthetic.Undecidability Undecidability.MinskyMachines(ndMM2 ndMM2_undec) Undecidability.ILL(IMSELL ndMM2_IMSELL)