Optimize iDestruct by avoiding superfluous iRenames

This is not a major optimization, but it seems to be an optimization nonetheless, so I thought I'd submit it to at least get some measurements from existing iris projects. From a quick benchmark, on our project we get a ~7-8% speedup (but I expect the speedup to be lower in most cases).

The idea is to avoid unnecessary calls to iRename. Currently, when doing iDestruct "H" as "[H1 H2]", iDestruct will produce two hypotheses, generating a fresh name for the first one and reusing "H" for the second one, then will call itself recursively, renaming each hypothesis into "H1"/"H2".

These final calls to iRename are superfluous, because we could have chosen the right names directly, and those iRenames can add up to 25-30% of the time taken by iDestruct (it's the eapply of the renaming lemma that takes time, I guess just because of unification).

The first commit of the PR optimizes the split case of iDestruct (as "[H1 H2]"), as this is what I expect to be the most common use of iDestruct. The second commit optimizes the IIntuitionistic/ISpatial/IModalElim cases; the change is slightly more intrusive, as it requires generalizing the corresponding lemmas to include a renaming step.

I ran a couple synthetic microbenchmarks to confirm that this is actually achieving something.

idestruct_bench.v: https://gitlab.mpi-sws.org/-/snippets/1701 (testing the first commit) idestruct_bench_2.v: https://gitlab.mpi-sws.org/-/snippets/1702 (testing the second commit)

idestruct_bench.v:

before:
Benchmark #1: coqc idestruct_bench.v
  Time (mean ± σ):      6.105 s ±  0.092 s    [User: 5.837 s, System: 0.238 s]
  Range (min … max):    5.920 s …  6.272 s    10 runs

after:
Benchmark #1: coqc idestruct_bench.v
  Time (mean ± σ):      4.370 s ±  0.071 s    [User: 4.135 s, System: 0.216 s]
  Range (min … max):    4.271 s …  4.522 s    10 runs

idestruct_bench_2.v:

before:
Benchmark #1: coqc idestruct_bench_2.v
  Time (mean ± σ):      6.228 s ±  0.240 s    [User: 5.973 s, System: 0.235 s]
  Range (min … max):    5.638 s …  6.475 s    15 runs

after:
Benchmark #1: coqc idestruct_bench_2.v
  Time (mean ± σ):      4.644 s ±  0.442 s    [User: 4.420 s, System: 0.208 s]
  Range (min … max):    4.057 s …  5.202 s    15 runs

The measurements are kind of noisy, I suspect because part of the time is spent just doing I/O to load the iris theories; but nevertheless demonstrate that there is indeed a speedup +/- corresponding to the 25% of the time spent in iRename that I could measure before.