lib automath common basic_ag basic_rg complete_rg toplevel