The automatic lifting translation function, still with dummy types, but works everywhere in the LF example.

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

use_thys ["Paper"];