lib automath common basic_rg basic_ag toplevel