Stream: General

Topic: Eta expand for unfolding

view this post on Zulip Jan van Brügge (Jan 02 2022 at 19:12):

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