Introduced a new invariant on the inferencer

This adds quite a few (currently cheated) cases for showing that the
invariant is preserved.