Revert "Use implication in core so that we can test it.", add a dedicated test
This reverts commit daaabf41. We have tests for testcase, we shouldn't depend on using arcane features in our definitions for this purpose. Also, this exposes that there still is a bug somewhere (see the FIXME).
gen_proofmode in 23 minutes and 59 seconds (queued for 2 seconds)3 jobs for