∀ {α : Type u_1} (table : Array.PrefixTable α) (state : Fin (table.size + 1)) (table_1 : Array.PrefixTable α)
  (state_1 : Fin (table_1.size + 1)),
  ({ table := table, state := state } = { table := table_1, state := state_1 }) = (table = table_1 ∧ state ≍ state_1)