Derive contradictions about injective facts in the presence of last(-) formulas

In deriving contradictions about injective facts, we need three
timepoints i, j, k and an ordering i < j < k. When i < j and last(#k)
hold, such an ordering does exist, but j < k seems to be implicit. The
patch extends the check to cover that case as well (note that j /= k is
already checked for before).