Better way of writing `Proper` premises in fin sets

Use Proper (.. => impl) instead of Proper (.. => iff) and ∀ x, Proper .. instead of Proper ((=) ==> ..).

The new premises are easier to prove (both solve_proper and manual proof).

This came up in !478 (merged)