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