law reverse_replicate_sym

bend-mathlib@0.8.1.0 · list.bend:2727

import Base

2727# Reversing n copies of x gives them back, reversed to rewrite toward the simple side.
2728law reverse_replicate_sym:
2729  for -A: Data
2730  for n: Nat
2731  for -x: A
2732  {List.replicate(A, n, x) == List.reverse(&2, A, List.replicate(A, n, x)) : List<&2, A>}