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).
Merge pull request #138 from oggy-/develop

Reasoning about inductive facts ignores "last" formulas

Thanks @oggy- for the change and the explanation. I can now seee that the soundness proofs extends properly.