refactor(library/definitional): combine auxiliary functions used by definitional package in a single module
refactor(library/definitional/util): remove code duplication
feat(definitional/brec_on): add 'mk_below' skeleton
fix(library/definitional/cases_on): bug in inductive datatypes with higher-order recursion
refactor(library/definitional/no_confusion): cleanup API
test(tests/lean/run): test brec_on on vectors
feat(library/data/vector): expand 'vector' module
feat(frontends/lean/inductive_cmd): improve resulting universe level inference for inductive datatypes

The new test contains examples that required explicit levels.
test(tests/lean/run): define brec_on and binduction_on for a reflexive type

We say an inductive type T is reflexive if it contains at least one constructor that
takes as an argument a function returning T.

For reflexive types it doesn't seen to be possible to define a single
brec_on that can eliminate to Type.{>=1} and Prop.
The universe level expressions get too complicated.
Even if we extend the universe constraint solver in the kernel, the
additional complexity might be a problem.

We workaround this issue by defining two versions of brec_on:
  - One (brec_on) that eliminates to Type.{>=1}, and
  - binduction_on that eliminates to Prop.

For non-reflexive types, we can combine both of them.