The Productive use of Failure to Generate Witnesses from Divergent Proof Attempts for Coinduction - Dennis, Louise Abigail; Bundy, Alan; Green, Ian (Kluwer, 2000)
Coinduction is a proof rule. It is the dual of induction. It allows reasoning about non--well--founded structures such as lazy lists or streams and is of particular use for reasoning about equivalences. A central difficulty in the automation of coinductive proof is the choice of a relation (called a bisimulation).