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.

assigned to @robbertkrebbers

changed the description

I can't see anything obviously wrong this this MR. I also don't know our existing Proper instances for these things so I cannot tell if any of the new instances is (partially) redundant -- I trust you checked that.

resolved all threads

added 7 commits

• b7b87501...06909b86 - 3 commits from branch master
• d40e0d65 - Add missing `Params` instances.
• c67f7331 - Use "higher-order" propers for list operations.
• cce709e0 - Add some tests for backwards compatibility.
• 0387d97b - Fix `Params` for `alter` and add a test.

Compare with previous version

Going to merge.

merged

mentioned in commit 66a28855

mentioned in commit iris@efc49b45

mentioned in merge request iris!837 (merged)