There are straightforward instances of `Proper (R ==> R) (λ x, x)`

and, assuming f and g are proper, `Proper (R₁ ==> R₃) (λ x, g (f x))`

. Do I need to declare these or are the tactics smart enough to find them?

no, but

if you _name_ g (f x), yes. stdpp’s `solve_proper`

finds those. the stdlib has a solve_proper, but I never tried it.

but otherwise, `rewrite`

will search separately for instances for `f`

and `g`

Last updated: Oct 03 2023 at 02:34 UTC