Tentative patch for incompatibility between subterm relation and dependent
pattern matching.

This patch should be improved in two ways:
(1) Implement the same checks for the commutative cut subterm rule.
(2) When checking safe recursive subterms for each of the branches in a match,
instanciated parameters in the return predicate should be taken into account.

Step (1) should be enough to restore a correct guard condition, but (2) will
be required if we don't want to rule out some legitimate and practical examples.
Tentative fix for the commutative cut subterm rule.

Some fixpoints are now rejected in the standard library, but that's probably
because we compare trees for equality instead of intersecting them.
Refining match subterm and commutative cut rules. The parameters that are
instantiated in the return predicate are now taken into account. The resulting
recargs tree is the intersection between the one of the branches and the
appearing in the return predicate. Both the domain and co-domain are filtered.
Made intersection on regular trees less intensional.
Fixed proof of irrelevance of le on nat, inspired by the
corresponding proof in ssreflect.
A version of Fin.rect2 that is compatible with the fix of the guard condition.

Thanks to Arthur Azevedo de Amorim!
Simplified rect2, it turns out Arthur's trick was not required.

Standard library now compiles fully.
Typo in comment.
Add test-suite file for guard condition on cofixpoints.
First attempt at a fix for guard condition on cofixpoints.
Refined guard condition of cofixpoints, to anticipate potential futur
extensions.
Refine check_is_subterm.

Following Bruno's suggestion, we check if the tree expected for the recursive
argument is included in the one which is inferred.  This check is probably
not necessary in the current state of affairs, but might become so after
further extensions of the guard condition.
Fix check_inductive_codomain.
Extend subterm relation to pattern matching in return predicates.

A pattern matching is can now be a subterm if:
- Every branch is a subterm
- The return predicate is a pattern matching whose return predicate is an arity.
- That pattern matching (in the return predicate) returns the same inductive
family in the conclusion of each branch.

The commutative cut rule hasn't been updated accordingly yet.
Propagate size info through pattern matching in predicates, for the
commutative cut rule.

The error messages of the guard checker are now sometimes not
informative enough.
Revert "Propagate size info through pattern matching in predicates, for the"

This reverts commit 6a3bcd3ae320e65347cbd6ef4bac458f073d02ea.

Apply again if this kind of dependently typed programming idioms are needed.
Revert "Extend subterm relation to pattern matching in return predicates."

This reverts commit ec1bb8a981fef14b58ab65483244fc42b05aef13.
Minor cleaning.
Porting guard fix to checker.
Change the interface of proof_global to take an evar_map instead of a universe context to start proofs.

It was kind of awkward to work with for non-traditionnal kinds of proofs: if you have an evar_universe_context, you got it from a sigma anyway.