fin_maps: generalise map currying/uncurrying

All these proofs basically transfer directly to any finite map, which is a change I want to make in advance of upstreaming more theory around uncurrying. There was a small change due to the use of transitivity not terminating for arbitrary finite maps, presumably due to some kind of typeclass shenanigans. I just made the proof more explicit in rewriting to get it to work again.