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?
if you _name_ g (f x), yes. stdpp’s
solve_proper finds those. the stdlib has a solve_proper, but I never tried it.
rewrite will search separately for instances for
Last updated: Jan 28 2023 at 05:02 UTC