Alternative fixes for iris!886 that do not rely on backwards compatibility layer

This MR does no not rely on dist_later_fin, but uses the new dist_later directly.

I realized that f_contractive_core is a useful tactic if the Contractive instance is manually applied (because TC search cannot find it), and you need to introduce the dist_later yourself. I will later make an Iris MR to (a) rename f_contractive_core into dist_later_intro (b) make clear that dist_later_intro is not just something internal (c) allow one to omit arguments of dist_later_intro.