Parameters of existential types first commit: connect the argument variables to parameter instances of the postcondition; prune the solution of the old arguments since each iteration derives fresh postconditions. Does not prune enough yet.