law Deque.pop_back.push_back

bend-kit-collections@0.1.4.1 · deque.bend:197

import Base

197# LAW: pop_back undoes push_back
198law Deque.pop_back.push_back:
199  for -A: Data
200  for -x: A
201  for  d: Deque<&2, A>
202  {Deque.pop_back(&2, A, Deque.push_back(&2, A, x, d))
203   == Some{(x, d)} : Maybe<&1, A & Deque<&2, A>>}