law length_append_sym

bend-mathlib@0.8.1.0 · string.bend:558

import Base

558# The length of an append is the sum of the lengths, reversed to rewrite toward the simple side.
559law length_append_sym:
560  for a: String
561  for -b: String
562  {Nat.add(String.length(a), String.length(b)) == String.length(String.append(a, b)) : Nat}