perf: override the data structures of coinductive types

[Komyyy]

The data structures of the model of coinductive types (Stream', Computation, Stream'.Seq) are inefficient, so we override their data structures.

---

• depends on: [Merged by Bors] - style: rename Stream'.nth to Stream'.get #7514
• depends on: feat: opaque_repr attribute to suppress "trivial structure" opt leanprover/lean4#2292
• depends on: refactor: specialize Acc.rec and WellFounded.fix batteries#371
• depends on: [Merged by Bors] - chore: bump Std #8460