A concrete example, with a proof that rbv is not regular and with proofs of induction and pseudo-injectivity that require this

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

use_thys ["Paper"];