We can use the induction hypothesis when we are proving a property for a structure that is well-ordered. I am aware that there is a proof for this.

When it comes to coinduction, I’m confused.

One of the answers to another question “What is coinduction?” mentions that there is a notion of a corecursive definition to be well-formed.

A lot of things I (try to) read related to coinduction mostly talk about bisimulation and equivalence. But to the best of my knowledge, those are trying to prove some relationship for two coinductive data structures. For example, they prove that two streams are equivalent. And the coinductive hypothesis is somehow derived from one of the bisimulation’s hypothesis. Even so, I think I’m still lost on the requirements of what constitutes well-formedness in the coinductive world.

I can somehow see that the coinduction hypothesis works when proving those kinds of propositions, but I’m still unclear when they can be used to prove more general propositions such as the one mentioned in What is coinduction?. In that link, the proposition states that “something is infinite”. This seems like a more generic form of statement one would be interested in proving.

A possibly related question is whether any proposition can be converted and re-stated as a proposition of equivalence or not.

Is there some simple informal reasoning that talks why co-induction works for some well-formedness requirement?

I’m hoping for an explanation like if possible: https://math.stackexchange.com/questions/432293/well-ordering-and-mathematical-induction/432302#432302.