the chk-functions in quotient_term also simplify the result according to the id_simps; had to remove id_def from this theorem list though; this caused in FSet3 that relied on this rule; the problem is marked with "ID PROBLEM"

     1

no_document use_thys ["../Quot/QuotMain"];

     2

     3

use_thys ["Paper"];