feat(util/list): add to_list from buffer
refactor(library/util): allow mk_telescopic_eq to be used with (terms, locals)
feat(library/util): add mk_heq
feat(library/util): add mk_refl
feat(hott/init): add proof for Hedberg's theorem
feat(hott/init): add auxiliary definition needed by definitional package
refactor(frontends/lean): move choice_iterator to library
refactor(frontends/lean): move type_checker_ptr typedef to library
refactor(frontends/lean): move pp_options to library
refactor(frontends/lean/placeholder_elaborator): reduce coupling between placeholder_elaborator and frontends/lean
refactor(frontends/lean): move some auxiliary procedures to library/tactic
refactor(frontends/lean): move placeholder_elaborator to library/tactic
feat(hott/init/datatypes): add sum.intro_left and sum.intro_right aliases
refactor(library/init/datatypes): change implicit arguments of sum.inl and sum.inr
refactor(library/init/sigma): rename sigma.dpair->sigma.mk, sigma.dpr1->sigma.pr1, sigma.dpr2->sigma.pr2
refactor(hott): use same name convention for sigma in the HoTT and standard libraries
fix(hott/init/hedberg): remove unnecessary import
refactor(library/tactic): rename placeholder_elaborator to class_instance_synth
feat(library/tactic/class_instance_synth): add mk_class_instance procedures
fix(hott/init): minimize number of universe parameters