This talk will explain the each word in the title separately, and then how they can be combined together. Our problem is how to make coinductive equivalence proofs easier, and in particular how to prove sound enhancements of the bisimulation proof technique (also called up-to techniques). The lingua franca of this talk will be the lambda-calculus.