feat(frontends/lean/server): add VISIT and CHECK commands

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(frontends/lean): add '#erase_cache' command (for debugging purposes)

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
fix(library/unifier): bug in mk_imitiation_arg

Remove bogus constraint
     cs.push_back(mk_eq_cnstr(mk_app(maux_type, locals), type, j, relax));
This constraint is incorrect because 'type' may contain local constants that are not in 'locals'.

We just rely on
   cs.push_back(mk_eq_cnstr(mk_app(maux, margs), arg, j, relax));
When maux is assigned, the system will inforce that its type (which is based on maux_type) must be type correct

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
test(tests/lean/slow): add self contained path_groupoids test file

Signed-off-by: Leonardo de Moura <leonardo@microsoft.com>
feat(library/standard): add classes for relations
feat(library/hott): begin porting Coq HoTT
refactor(library/standard): integrate hott with standard library