law reverse_append

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

import Base

35law reverse_append:
36  for -A: Data
37  for xs: List<&2, A>
38  for ys: List<&2, A>
39  {List.reverse.go(&2, A, List.reverse(&2, A, xs), ys)
40    == List.append(&2, A, xs, ys) : List<&2, A>}