law length_replicate

bend-mathlib@0.8.1.0 · list.bend:397

import Base

397# Replicating x n times gives a list of length n.
398law length_replicate:
399  for -A: Data
400  for n: Nat
401  for -x: A
402  {List.length(&2, A, List.replicate(A, n, x)) == n : Nat}