law concat_append

bend-mathlib@0.8.1.0 · list.bend:480

import Base

480# Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss.
481law concat_append:
482  for -a: Quant
483  for -A: Kind(a)
484  for xss: List<a, List<a, A>>
485  for -yss: List<a, List<a, A>>
486  {List.concat(a, A, List.append(a, List<a, A>, xss, yss)) == List.append(a, A, List.concat(a, A, xss), List.concat(a, A, yss)) : List<a, A>}