added eqvt-lemma for split; changed semantics of perm_simp: excluded stands for constants about which no complaint is written out...eqvt_apply is now always applied

quick_and_dirty := true;
no_document use_thys ["LaTeXsugar"];
use_thys ["Paper"];