CVLByExample/QuantifierExamples/DoublyLinkedList/certora/spec/dll-linkedcorrectly.spec has a confusing unused ghost

[banshee]

CVLByExample/QuantifierExamples/DoublyLinkedList/certora/spec/dll-linkedcorrectly.spec has these unused definitions:

ghost nextstar(address, address) returns bool {
    init_state axiom forall address x. forall address y. nextstar(x, y) == (x == y);
}
ghost prevstar(address, address) returns bool {
    init_state axiom forall address x. forall address y. prevstar(x, y) == (x == y);
}

It's confusing since they're never used. Either they should be removed, or code should be added to use them.

(I asked about this in discord)