Algebra.list_nat_append_assoc4: law of bend-mathlib@0.8.1.0
Import: import bend-mathlib@0.8.1.0/algebra.bend as Algebra
Lines 223-229 of bend-mathlib@0.8.1.0/algebra.bend: https://jend.leeeet.dev/read.txt?path=bend-mathlib@0.8.1.0/algebra.bend&start_line=223&end_line=229

import Base

# Four-way reassociation for List append over Nat.
law list_nat_append_assoc4:
  for +a: List<&2, Nat>
  for +b: List<&2, Nat>
  for +c: List<&2, Nat>
  for +d: List<&2, Nat>
  {List.append(&2, Nat, List.append(&2, Nat, List.append(&2, Nat, a, b), c), d) == List.append(&2, Nat, a, List.append(&2, Nat, b, List.append(&2, Nat, c, d))) : List<&2, Nat>}

Uses (5):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=internal_list_nat_append_assoc
  https://jend.leeeet.dev/definition.txt?path=bend-mathlib@0.8.1.0/algebra.bend&name=op_assoc4