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