Use with coinductive types.
Meaning:
Induction is a well-established proof principle that is taught in most undergraduate programs in mathematics and computer science. In computer science, it is used primarily to reason about inductively defined datatypes such as finite lists, finite trees and the natural numbers. Coinduction is the dual principle that can be used to reason about coinductive datatypes such as infinite streams or trees, but it is not as widespread or as well understood.
From "Practical coinduction" by Dexter Kozen and Alexandra Silva (pdf)
References:
nLab
"Practical coinduction" by Dexter Kozen and Alexandra Silva (pdf)
