Replacing equivp by reflp in the assumptions leads to non-provable subgoals in the gen_pre lemmas.

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

use_thys ["Paper"];