I have a quite vague and naïve question: what are the differences between the different proof assistants regarding coinduction?
My motivation is that I'd like to formalize some proofs, basically about coinductive λ-calculus (thus involving binders, reductions, quotient up to renaming of bound variables, etc. but also nested inductive and coinductive structures). However, I ask the question imprecisely since I didn't find many general answers on the web.
The proof assistants I am considering are: Coq, Lean and Agda. These are the main three that I'd like to compare, but I'm open to any suggestions.