Jan van Brügge (Jan 02 2022 at 19:12): 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