∀ {line : Std.Format} {column : ℕ} {tags : List (ℕ × Std.Format)} {line_1 : Std.Format} {column_1 : ℕ}
  {tags_1 : List (ℕ × Std.Format)},
  { line := line, column := column, tags := tags } = { line := line_1, column := column_1, tags := tags_1 } →
    line = line_1 ∧ column = column_1 ∧ tags = tags_1