yeah ive never heard anyone say they like doing productive coinduction in lean. agda almost has a story, but the ergonomics and semantics arent trivial.

though i have thought about it.