feat(library/hott) add the proof that the inverse of an equivalence is an equivalence

This is done by changing the order of theorems and using the adjointification.
fix(library/hott) fix strange commit
doc(intro): basic slides
fix(frontends/lean): missing type info in expressions nested in tactics
fix(build): do not disable unicode chars on Windows
refactor(library/tactic/goal): remove unnecessary parameter
feat(library/tactic/apply_tactic): modify heuristic for adding arguments to apply tactic.
feat(library/tactic): add generalize tactic, closes #34

Remark: the intros tactic has been added in a different commit: 7d0100a3400b70c19422c
fix(library/data/quotient/default.lean): remove classical
feat(frontends/lean): use nice names for meta-variables when executing `check c` and `c` is a constant
feat(frontends/lean): add 'print axioms' command, close #251
fix(library/tactic/expr_to_tactic): memory leak
fix(frontends/lean/tokens): typo