proposition: Lemma mk_pTM n (sig : finType) (m : TM sig n) : pTM sig unit n.
proof: Proof. unshelve econstructor. - exact m. - exact (fun _ => tt). Defined.
imports: Undecidability.TM(Single.StepTM TM) Undecidability.TM.Code.Code Undecidability.TM(Single.EncodeTapes) Undecidability.Synthetic.Definitions