Extend framework for specification inference?

[Gopiandcode]

This idea was suggested by @mkeoliya - one possible way we could use proof reduction in the future is to use it for specification inference as well. Given an OCaml program - as the OCaml typesystem provides some constraints, we can infer what the footprint of a program is quite easily. Then, we can look for any higher order functions in the body of a program, look up the lemmas of them in Coq, and use the proof reduction to quickly test out candidates.