On 09/09/2015 14:58, Lars Hupel wrote:
Hi Jasmin,If you disable eta-contraction in printing, with declare [[eta_contract = false]] you will see that the two terms are not exactly the same, which is enough to derail the simplification.thanks for the investigation. Apparently spontaneous eta-contraction is a tricky business. I just wonder why the 'induction' method appears to eta-expand terms occurring in my goal.
Induction performs resolution and resolution can eta-expand. Tobias
Description: S/MIME Cryptographic Signature