Integration Coq Formalization with LM Formalization

[andrew-johnson-4]

Coq Prop are sound but reallly nasty to use. For now the verifier can do projects to check nominal types, then project those nominal types onto their properties in Coq. This is a tradeoff from sound to unsound formalization.

It would be nice to integrate directly with Coq formalizations, but that would entail the generation of verbose proof tactics for every type definition. It is possible but would be extremely time consuming. For now the middle of the road option is to do model checking, but not an entire ground-up proof.