What about allowing several (non-ambiguous) names for arguments, e.g. with syntax:

```
Arguments Nat.add_assoc (n|x|n1)%nat (m|y|n2)%nat (p|z|n3)%nat.
```

or, maybe:

```
Arguments Nat.add_assoc (n m p)%nat, (x y z)%nat, (n1 n2 n3)%nat.
```

so that we can more flexibly adopt namings locally consistent within a file without having to change all theories depending on them?

I'm inspired by #18092 which merges two copies with different names of the statement of proof irrelevance while compcert assumes one of the two namings.

Last updated: Oct 13 2024 at 01:02 UTC