Generalize Propers for lists / Add some missing Params
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.
Edited by Ralf Jung