Solution

Extend specification queue3 to verify FIFO queues with no repetitions, enqueue and dequeue.

// queue7
// single FIFO queue with no repetitions, enqueue and dequeue

deq matches deq(_);

Main = Queue!; 
Queue={let val; enq(val) ((enq(val)* deq|Queue)/\(deq>>deq(val) all))};