law reverse_cons_sym

bend-mathlib@0.8.1.0 · list.bend:3142

import Base

3142# Reversing a cons puts its head last: reverse (x :: xs) = reverse xs ++ [x], reversed to rewrite toward the simple side.
3143law reverse_cons_sym:
3144  for -a: Quant
3145  for -A: Kind(a)
3146  for -x: A
3147  for xs: List<a, A>
3148  {List.append(a, A, List.reverse(a, A, xs), [x]) == List.reverse(a, A, x <> xs) : List<a, A>}