tried to witness the hom-lemma with the recursion combinator from rlam....does not work yet completely

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

use_thys ["Paper"];