l2s: proving invariant with theorem fails with syntax error

[nano-o]

The following fails with error: token 'proof': syntax error.

#lang ivy1.7

type t
relation r(X:t)

export action my_action = { r(X) := true }

axiom [test] {
    property true
}

temporal property forall X . eventually r(X)
proof {
    tactic l2s with
        invariant true
        proof {
            assume test
        }
}

[kenmcmil]

The proof at line 16 is not supported. I might consider that as a feature request. Do you have a use case for it?

[nano-o]

I do, but I might be able to get around it by using the theorem to prove a helper invariant outside the l2s tactic.