This instance might seem odd, but `ProofIrrel` takes a `Type` and not a `Prop`,
and stdpp already has instances for products.

Code not affected by a00d9bd8.

All occurrences are gone, except for one in `base.v` where you'd need different
functions.

However, I'm unsure this is an improvement: in lots of cases here, the function
didn't need to be guessed, but could be deduced by "simple" higher-order
unification, the one where unifying `?f ?a` against `g args last_arg` sets `?f =
g args`.

Code affected by a00d9bd8.

This was done using `sed --in-place 's/[[:space:]]\+$//' theories/*.v`.

This was inconsistent and not explained before.

Fix both an error by my, and a provide compatibility with older Coq versions
whose `lia` is less powerful.

For other operations, like `<$>`,  such lemmas appear to make little sense, since
they require premises involving `!!`.

This follows iris/iris!387
This closes issue #54.

This feature is now deprecated in Coq master (see
https://github.com/coq/coq/pull/7791).

Instead of passing a partially-applied lemma directly to Hint Resolve,
first create a definition and then make that reference a hint.

The opposite was true before to this commit.