Understanding rec

Stream: new members

[Felipe]

Hi I'm new to Lean/dependent types. I'm trying to understand the rec and rec_on eliminators in the non-trivial cases like https://stackoverflow.com/a/74397922/754254. Any good resources to recommend?

[Felipe]

I think I figured out what's going on, but would love some feedback on my thoughts! Posted as Q&A: https://proofassistants.stackexchange.com/q/1833/1808