law concat_append_sym

bend-mathlib@0.8.1.0 · list.bend:2458

import Base

2458# Concatenating an append concatenates each part: concat (xss ++ yss) = concat xss ++ concat yss, reversed to rewrite toward the simple side.
2459law concat_append_sym:
2460  for -a: Quant
2461  for -A: Kind(a)
2462  for xss: List<a, List<a, A>>
2463  for -yss: List<a, List<a, A>>
2464  {List.append(a, A, List.concat(a, A, xss), List.concat(a, A, yss)) == List.concat(a, A, List.append(a, List<a, A>, xss, yss)) : List<a, A>}