{Γ : Type u_1} →
  {Λ : Type u_2} →
    {inst : Inhabited Γ} →
      {P : Sort u} →
        {q : Λ} →
          {Tape : Turing.Tape Γ} →
            {q' : Λ} →
              {Tape' : Turing.Tape Γ} →
                { q := q, Tape := Tape } = { q := q', Tape := Tape' } → (q ≍ q' → Tape ≍ Tape' → P) → P