Chore: Fix copyright information

[markusdemedeiros]

Right now copyright (at the top of each file) is assigned to a bunch of random people. Who should we set this to? Something like "Iris maintainers" or something, I'm not sure though.

[MackieLoeffel]

I don't think it is actually necessary to put the authors at the top of every file. Git tracks authorship a lot better than these list of names. Also it is not legally necessary to have a license header in every file at all and we could consider getting rid of it completely. We could also look into a more minimal header. Here is a list of options for headers in the files (all of which would be legally ok, at least according to GPT-5.4 / Opus 4.6).

1. (no header)

module ...

/- SPDX-License-Identifier: Apache-2.0 -/
module ...

/- Copyright (c) 2026 The Iris Lean Authors
    SPDX-License-Identifier: Apache-2.0 -/
module ...

4. (current)

/-
Copyright (c) 2022 Lars König. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Authors: Lars König, Mario Carneiro, Michael Sammler, Yunsong Yang
-/
module ...

(The order of these options corresponds to my preference.)
Maybe @digama0 has an opinion on this?

[digama0]

Currently I've been following mathlib conventions, which is to put the first author on the copyright line and all people who touched the file significantly on the authors line. I don't like "Iris Maintainers", that just obscures the actual authorship. For something mathlib-sized this would be very misleading, but even here I think there is some variation in file authorship since it has changed hands a few times.