law append_assoc_sym

bend-mathlib@0.8.1.0 · string.bend:548

import bend-mathlib@0.8.1.0/string.bend as String
import Base

548# Append is associative: (a ++ b) ++ c = a ++ (b ++ c), reversed to rewrite toward the simple side.
549law append_assoc_sym:
550  for a: String
551  for -b: String
552  for -c: String
553  {String.append(a, String.append(b, c)) == String.append(String.append(a, b), c) : String}

Uses (4)

Used by (0)

No other definition uses this definition.