law reverse_append_sym

bend-mathlib@0.8.1.0 · list.bend:2182

import Base

2182# Reversing an append reverses and swaps the parts: reverse (xs ++ ys) = reverse ys ++ reverse xs, reversed to rewrite toward the simple side.
2183law reverse_append_sym:
2184  for -a: Quant
2185  for -A: Kind(a)
2186  for xs: List<a, A>
2187  for ys: List<a, A>
2188  {List.append(a, A, List.reverse(a, A, ys), List.reverse(a, A, xs)) == List.reverse(a, A, List.append(a, A, xs, ys)) : List<a, A>}