law reverse_singleton

bend-mathlib@0.8.1.0 · list.bend:387

import Base

387# Reversing a one-element list gives it back.
388law reverse_singleton:
389  for -a: Quant
390  for -A: Kind(a)
391  for -x: A
392  {List.reverse(a, A, [x]) == [x] : List<a, A>}