Remove formula_prop and add shallowly-embedded formulas

[skeuchel]

The Inst instances for Formula and PathCondition that instantiate them to Prop are inconsistent with how Inst is used in all the other cases. The Prop type represents the interpretation of Formulas in the model. This is particularly awkward when it comes to lifting which uses formula_prop and for the laws of the type class which use equality rather than a configurable setoid (bi-implication) on the instantiated type. A cleaner way would be to remove the instances again and use bespoke inst functions as before, or even to create a shallow-embedding of formulas akin to all the other Inst cases.

With this change, formula_prop becomes unnecessary and can be removed. This is turn would make formulas and even complete verification conditions first-order. This means we could extract the symbolic executor, run the compiled version and pretty-print the resulting verification conditions.