This change adds embedded formatting metadata to week-04_backward-and-forward-proofs.v, including title, authorship, date, and table-of-contents directives for PDF generation. It doesn’t alter any proof logic, but it improves how the exercise material is exported and presented outside the Coq editor. The practical effect is a more polished PDF output for sharing or submission.