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/hott) ported Pointed.v
feat(library/hott) port a good portion of FunextVarieties.v
feat(library/hott) port the rest of Funext_Varieties.v
chore(library/hott) cleaned up the proof a bit
feat(library/hott) Ported part of UnivalenceImpliesFunext.v
feat(library/hott) add to trunc.lean: contractible types are equivalent to unit
feat(library/hott) almost completed portin UnivalenceImpliesFunext.v
fix(library/hott) changed pointed.lean to use trunc.lean correctly
chore(library/hott) remove hott.axoims.ua from imports of funext_from_ua.lean
feat(library/algebra/group): add theorems for calculation
feat(library/hott) postcomposition from ua lemma is done up to the last gap
chore(library/hott) fix universe issue. note: this should be fixed when contr is not bound to universe level 1 anymore