Jan van Brügge (Jul 31 2022 at 18:23): Jan van Brügge (Jul 31 2022 at 18:23):Hi, is there a way to restrict a unfolding so it does not do eta expansion?
I am trying to use comp_apply in a lemma that looks like P (a ∘ b) ((g ∘ h) x). Unfolding comp_apply does not result in P (a ∘ b) (g (h x)), but in P (λx. a (b x)) (g (h x)). Is there a way to prevent this from happening?
Jan van Brügge (Jul 31 2022 at 18:24):at the moment i am working around it with some deeply nested arg_cong, but a proper solution would be much nicer
Last updated: Nov 13 2025 at 04:27 UTC