law reverse_twice

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/sha/list_proofs.bend:20

import Base

20law reverse_twice:
21  for -A: Data
22  for xs: List<&2, A>
23  for acc: List<&2, A>
24  for ys: List<&2, A>
25  {List.reverse.go(&2, A, List.reverse.go(&2, A, xs, acc), ys)
26    == List.reverse.go(&2, A, acc, List.append(&2, A, xs, ys)) : List<&2, A>}