Replace unused pattern variables with underscore

Addresses new unused-pattern-matching-variable warning on Coq master (see https://github.com/coq/coq/pull/12768).

I'm pretty sure the hlist.v warning is a bug in Coq's heuristics for this, since those variables are used as implicit arguments and I don't see why the pattern matches more than one case (the warning is also printed twice for the same definition). Maybe there's something in the elaborated term I'm missing, which Coq doesn't even print back?

Regardless of what's going on in Coq, it's much easier for us to suppress the warning than to try to fix this upstream.