Parameterized Coinduction

[hxrts]

Hi there, I've been working on some proofs that required coinductive techniques and found myself having to work outside Mathlib. I ended up building a faithful port of Paco from Coq → Lean so I could work with known proof techniques.

Original: https://github.com/snu-sf/paco

Lean version: https://github.com/hxrts/paco-lean

Differences between the two: https://hxrts.com/paco-lean/07-coq-differences.html

I'm happy to keep this as a separate library, but it seems like common machinery of this sort tends to end up in Mathlib, so I thought I'd ask if this seemed of use to the Mathlib community. If so, I can split it up into a few PRs, or follow contributor guidance for inclusion.

Thanks!