either print fully concrete counterexample or admit we fail to find one

This pull request:
* ensures the counterexample is always fully concrete
* remembers equations between arguments and results
* simplifies and improves precision of  `δσ^` for division by using the provability relation rather than doing manual checking
* adds more examples for printing counterexamples