Eduardo Freire (Aug 11 2022 at 17:26): Eduardo Freire (Aug 11 2022 at 17:26):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!
Notification Bot (Aug 11 2022 at 17:27):Eduardo Freire has marked this topic as resolved.
Pierre Courtieu (Aug 12 2022 at 08:44):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