Create a CLI command that copies generated Lean code back into Rust file or a separate file

[abentkamp]

A user edits the Lean proofs directly in the generated Lean file. When done, they can run a CLI command to copy the proofs from Lean into Rust annotations or into a separate (JSON?) file. To do this, we will need some magic comments in the Lean file to mark the relevant sections. When running cargo hax into lean again, the Lean file will be overwritten, using the Rust annotations or the JSON file contents as proofs.