feat: graft imported informal proof bodies

[ejgallego]

This PR lets explicit proof grafts render an imported attribute-backed informal proof without including its original Verso document as content.

• Reconstruct the requested proof facet through the existing placement and rendering path, preserving dependency axes, numbering, destinations, and folding.
• Keep default grafts and module inclusion statement-only. Missing informal proof bodies retain the unavailable-facet notice; compiled Lean proofs and dependency-only metadata are not substituted for prose.
• Cover transitive imports, separate proof contributors, repeated placements, ordinary document inclusion, and manifest/cache and saved-state round trips; update the authoring and API documentation.

Backport v4.33.0: #454

Prepared with Codex using GTP-6