More work on fixing the inferencer soundness proof.

It much more tricky than I thought it would be.