law replicate_add_sym

bend-mathlib@0.8.1.0 · list.bend:2716

import Base

2716# Replicating m + n times appends m copies to n copies, reversed to rewrite toward the simple side.
2717law replicate_add_sym:
2718  for -A: Data
2719  for m: Nat
2720  for -n: Nat
2721  for -x: A
2722  {List.append(&2, A, List.replicate(A, m, x), List.replicate(A, n, x)) == List.replicate(A, Nat.add(m, n), x) : List<&2, A>}