Fixes around `converge` (convergence of postconditions).
Bug fix in renaming that lifts postcondition parameters from abduced parts.