test(tests/lean/run): pre-quotient experiment
feat(library/algebra/group): add ordered semigroups
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
fix(library/hott) adapt trunc.lean to missing equiv coercion
feat(library/data): define 'nat.addl' addition using recursion on the first argument, prove it to be equivalent to 'add', and use it to define vector.append
feat(library/data/nat/order): add calc_trans commands for lt and le
feat(library/data/fin): add fin type
test(tests/lean/run): define div using wf package
refactor(library/logic): add basic definitions for relations at logic/relation.lean

We need them for wf and definitional package
refactor(library/data/nat/sub): cleanup 'max' theorems
test(tests/lean/run/tree_height): experiment with wf relation based on the height

This is easier to generate than the subterm relation
test(tests/lean/run/div_wf): cleanup
test(tests/lean/run/gcd): gcd compiled by hand into wf recursion
fix(library/logic/wf_k): missing file
fix(frontends/lean): tactic + section variables, fixes #332
feat(library/hott) add universe polymorphism to paths, truncation, etc... get stuck at ua to funext proof anyway
feat(library/hott) completed the funext_from_ua proof with a somewhat restricted generality on universe levels
refactor(library/logic/decidable): rename decidable_rel -> decidable_pred, and decidable_rel2 -> decidable_rel
refactor(library/logic/prop): allow 'absurd' to generate Type