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.