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