added an example that recurses over two arguments; the interesting proof-obligation is not yet done

use_thys ["Paper"];