Proof search now also tries recursive calls

Though not at the top level, only under a constructor, to avoid
searching forever. (This can probably be improved simply to ensure that
it doesn't try applying the top level function.)