∀ {Γ₀ Γ₁ : Type} {tm : Turing.FinTM2} {inputAlphabet : tm.Γ tm.k₀ ≃ Γ₀} {outputAlphabet : tm.Γ tm.k₁ ≃ Γ₁}
  {tm_1 : Turing.FinTM2} {inputAlphabet_1 : tm_1.Γ tm_1.k₀ ≃ Γ₀} {outputAlphabet_1 : tm_1.Γ tm_1.k₁ ≃ Γ₁},
  { tm := tm, inputAlphabet := inputAlphabet, outputAlphabet := outputAlphabet } =
      { tm := tm_1, inputAlphabet := inputAlphabet_1, outputAlphabet := outputAlphabet_1 } →
    tm = tm_1 ∧ inputAlphabet ≍ inputAlphabet_1 ∧ outputAlphabet ≍ outputAlphabet_1