eval_match should not destruct user-written quantifiers.
For this purpose it preserves all quantifiers inside annotations.
For the same purpose it now also preserves all quantifiers appearing
inside terms in let-bindings (in particular, inside lambdas).