Eliminate parsing of proof scripts

[kiranandcode]

Currently the mechanism for handling old proofs is very ad-hoc - it involves parsing the old proof script using Coq, and then extracting the raw ast of any expressions in the proof script into our internal logical expression encoding.

This is problematic as it relies on the user adhering to particular proof styles, and is also very fragile - if the user defines additional notations, etc. we may misinterpret the resulting ast and waste time on ill-typed invariants.

A better approach would be to operate on the old proof term directly, analyze it and extract expressions from the proof term itself. This way, we are agnostic to the tactics and proof style and notations, and instead can observe exactly the expressions used by the user.

[kiranandcode]

Shifting our analysis of the old proof from the script to the proof term would also pave the way towards more principaled analyses of old proofs.