1 quick_and_dirty := true;
2 no_document use_thys ["LaTeXsugar", "../Nominal/FSet"];
2 no_document use_thys ["LaTeXsugar"];
3 use_thys ["Paper"];