law replicate_add

bend-mathlib@0.8.1.0 · list.bend:1339

import Base

1339# Replicating m + n times appends m copies to n copies.
1340law replicate_add:
1341  for -A: Data
1342  for m: Nat
1343  for -n: Nat
1344  for -x: A
1345  {List.replicate(A, Nat.add(m, n), x) == List.append(&2, A, List.replicate(A, m, x), List.replicate(A, n, x)) : List<&2, A>}