law reverse_replicate

bend-mathlib@0.8.1.0 · list.bend:1379

import Base

1379# Reversing n copies of x gives them back.
1380law reverse_replicate:
1381  for -A: Data
1382  for n: Nat
1383  for -x: A
1384  {List.reverse(&2, A, List.replicate(A, n, x)) == List.replicate(A, n, x) : List<&2, A>}