A few improvements to the Ivy proof

[nano-o]

• Restructure the induction proof for clarity.
• Remove one quantifier-alternation cycle (now the main accountability proof is fully in EPR).
• Some other minor fixes (the typo in network_shim.ivy could have been bad as it meant that the concrete pre-commit handler was never called; however it didn't affect the abstract pre-commit handler, and since most of the proof happens at the abstract level, fixing the typo didn't break the proof)