Sort u →
  {K : Type u_1} →
    {Γ : K → Type u_2} →
      {Λ : Type u_3} →
        {σ : Type u_4} →
          Turing.TM2to1.Λ' K Γ Λ σ →
            {K' : Type u_1} →
              {Γ' : K' → Type u_2} → {Λ' : Type u_3} → {σ' : Type u_4} → Turing.TM2to1.Λ' K' Γ' Λ' σ' → Sort u