Ah, this helped me find what I was looking for. Apparently the `Function`

package automatically defines `bubble_equation`

, which is the unfolding lemma I wanted. I will definitely look into `Equations`

though, thank you!

Eduardo Freire has marked this topic as resolved.

You have equation and induction lemmas defined automatically (for non dependently typed functions only). But indeed Function is getting old and Equations subsumes it almost every aspects.

Last updated: Feb 06 2023 at 12:04 UTC