Hmm, I was more thinking about proof translation across isomorphisms. I'm not speaking from my own experience here, just that I have seen people grumble about i

Hmm, I was more thinking about proof translation across isomorphisms. I'm not speaking from my own experience here, just that I have seen people grumble about it. https://leanprover-community.github.io/archive/113488general/20549invalidoccurrenceofrecursivearg10ofrvecparamvcons.html https://leanprover-community.github.io/archive/113488general...