fix: report `Std.Do` goals and a missing `Std.WP` import in `vcgen`

This PR makes `vcgen` report an error that names the fix when the goal is a `Std.Do` triple or entailment, and when `Std.WP` is not imported. The `Std.Do` error asks the user to restate the goal with the definitions from `Std.WP`, and to add `import Std.WP` when it is missing.

Closes #15691.

Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
Claude-Session: https://claude.ai/code/session_01D74FF4ctEFXXRh47PAFr7z