To call quotient it is enough to export the alpha frees to proper constants and their respective equivp theorems.

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

use_thys ["Paper"];