Deliverables:

• Extract a self-contained Noir file to a Lean file with parseable syntax
• Demonstrate the ability to reason about the resulting Lean nr_defs