  We propose a new cyclic proof system for automated, equational reasoning
about the behaviour of pure functional programs. The key to the system is the
way in which cyclic proof and equational reasoning are mediated by the use of
contextual substitution as a cut rule. We show that our system, although
simple, already subsumes several of the approaches to implicit induction
variously known as "inductionless induction", "rewriting induction", and "proof
by consistency". By restricting the form of the traces, we show that global
correctness in our system can be verified incrementally, taking advantage of
the well-known size-change principle, which leads to an efficient
implementation of proof search. Our CycleQ tool, accessible as a GHC plugin,
shows promising results on a number of standard benchmarks.
