quick_and_dirty := true; no_document use_thys ["Nominal2_Base", "Nominal2_Eqvt", "Nominal2_Atoms", "Nominal2_Supp", "Test", "Term1", "Term2", "Term3", "Term4", "Term5", "Term6", "Term7", "Term8", "Term9", "TySch", "LFex"];