Work out why test/WildCat/Opposite.v is slow about coq-hott

[jdchristensen]

I just realized that my comment at #1929 (comment) was confused. In that spot of that PR, what is being used is that op is involutive. Here, core5 is checking that core and op commute. So it's not weird that one of them (here) is slow while the other (in that PR) is fast. This one is probably slow simply because there is a huge amount to unpack. So this can probably be closed. (Although it would be nice if there was a way to make this fast...)

[Alizter]

Yes, looking back I think you are right. The issue here which perplexes me is that all of these examples in the test are instant except for is1cat. I tried for an hour today to get a favourable manual reduction but the term is just so huge. I also tried tweaking the proofs Equiv.v about core so that they are as eta reduced as possible. I cannot workout why this is such a straining example for Coq.