[REQ] Add indication for vacuous proofs

[leonardolima]

Is your feature request related to a problem? Please describe.

Considering the inputs

Signature:
p(x:int)
q(x:int)

Formula:
p(x) S[1,2] q(x)

Trace:
@1 q(1) q(2)
@1 p(1) p(3)
@2 p(1) p(2) p(3)
@5

The violation at time-point 0 does not point anywhere in the trace. Specifically, this happens because the corresponding proof (the PDT here is trivial) corresponds to VSinceOut 0. Such proofs (e.g., VPrevOutL, VPrevOutR, ...) do not contain subproofs and it is not yet clear how they should be presented.

Describe the solution you'd like

There should be an annotation somewhere pointing it out.

Describe alternatives you've considered

The annotation could potentially be included in the hovering table.

Additional context

No additional context.