fix: include star-indexed lemmas with `+all` when partial results exist

When using `apply? +all`, star-indexed lemma fallback was incorrectly
skipped whenever the primary search found any results (even partial
ones). The condition `!results.isEmpty` caused star lemmas to be
skipped even when only partial solutions existed.

Now with `collectAll=true`, star lemmas are searched unless a complete
solution was already found. Results from both primary search and star
search are combined when `collectAll=true`.

🤖 Generated with [Claude Code](https://claude.com/claude-code)

Co-Authored-By: Claude Opus 4.5 <noreply@anthropic.com>