For example, for fmap:
- Old:
Proper ((≡) ==> (≡)) f → Proper ((≡) ==> (≡)) (fmap f)
- New:
Proper (((≡) ==> (≡)) ==> (≡@{list A}) ==> (≡@{list B})) fmap
This means that solve_proper
can also find a Proper
instance when the two functions are different, and then prove that they are extensionally equal.
This is similar to what we have done in !276 (merged) for maps.