minor proof factorization
clean up
remove unused dirty_push from Deque.v