Universes clause check

[mattam82]

This PR adds a new loop-checking algorithm to MetaCoq, which should allow to handle arbitrary universe constraints efficiently, e.g. max (u + 1, v) = max (j, k+ 2). It is based on a constructive proof by Bezem et Coquand for the slightly more general problem of building a model in N^∞ of a set of horn clauses of shape u + k \/ ... \/ l + n -> l' + k'. This can be restricted to check if a loop follows from a set of constraints or if we have a model in N, which can in turn be seen as a valuation of the clauses making them all (non-vacuously) true.

The algorithm is currently only shown to be terminating and to return a valid model when it finds one, but it might also answer Loop, in which case we have not (yet) proven that there is indeed a loop.

I added a new extracted plugin in the test-suite (based on plugin-demo), that provides a new command MetaCoq Check Universes that checks for a model using the new algorithm on all the constraints in the global environment at the point of the call. It currently takes < 0.5s to verify that there is a valuation with 4 distinct universes for all the universes and constraints in Coq's standard library.