refactor(library/definitional): add some helper functions
fix(frontends/lean/inductive_cmd): bug in inductive datatype elaborator
refactor(library/definitional): add new to_telescope procedure, and remove code duplication in no_confusion.cpp
fix(library/definitional): marking cases_on and rec_on as reducible

The idea is to avoid counter-intuitive behavior
test(tests/lean/run/nateq): add example that triggered previous modification
feat(library/definitional): define ibelow and below

These are helper definitions for brec_on and binduction_on
fix(library/logic): import prod and unit declarations in logic

Reason: we need them for automatically generating constructions needed
by the definitional package
feat(library/unifier): solved universe constraints of the form succ^k1 a = max k2 ?m (when k1 >= k2)
feat(library/unifier): solved universe constraints of the form succ^k1 a = max k2 ?m (when k1 >= k2)