law length_replicate_sym

bend-mathlib@0.8.1.0 · list.bend:2397

import Base

2397# Replicating x n times gives a list of length n, reversed to rewrite toward the simple side.
2398law length_replicate_sym:
2399  for -A: Data
2400  for n: Nat
2401  for -x: A
2402  {n == List.length(&2, A, List.replicate(A, n, x)) : Nat}