I have a proof goal in the form of: `g A B (λx. f A B (h x)) C D = foo`

and a theorem like: `f ?A ?B (h ?x) ?y = bar ?x ?y`

that I want to use as an unfold rule. But the rule does not do anything because I need to eta-expand the lambda in my proof goal. How would I do that? (alternatively, getting rid of the `?y`

in the theorem would work too)

Last updated: Jul 15 2022 at 23:21 UTC