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.