Reasoning about inductive facts ignores "last" formulas

Reasoning about injective facts requires three timepoints i, j, k, such that i < j < k. When last(k) holds, the temporal ordering between j and k is apparently implicit. Currently, this causes Tamarin to fail to derive a contradiction, even when one exists. An example follows (Tamarin fails to prove the lemma).

    theory Last_Injective
    begin
    
    rule New_Loop:
        [ Fr(~x) ]
        --[ New_Loop(~x) ]->
        [ Loop(~x, '1') ]
    
    rule Start_Loop:
        [ Loop(x, '1') ]
        --[ Start_Loop(x) ]->
        [ Loop(x, '2') ]
    
    rule Do_Loop:
        [ Loop(x, '2') ]
        --[ In_Loop(x) ]->
        [ Loop(x, '2') ]
    
    rule Stop_Loop:
        [ Loop(x, '2') ]
        --[ Stop_Loop(x) ]->
        [ Loop(x, '1') ]
    
    lemma No_Stop_In_Loop[use_induction]:
        "All x #i.
            In_Loop(x) @ i ==> (
                Ex #j. Start_Loop(x) @ j
                    & j < i
                    & (All #k. Stop_Loop(x) @ k ==> k < j | i < k)
            )
        "
            
    end