I wrote a paper on this a few years ago http://moskal.me/pdf/prtrig.pdf though indeed getting the quantifiers to verify is more art than science...