lib automath common basic_ag basic_rg dual_rg toplevel