Prufrock: a framework for constructing polytypic theorem provers