law is_empty_append_sym

bend-mathlib@0.8.1.0 · string.bend:656

import Base

656# An append is empty exactly when both parts are, reversed to rewrite toward the simple side.
657law is_empty_append_sym:
658  for a: String
659  for -b: String
660  {Bool.and(String.is_empty(a), String.is_empty(b)) == String.is_empty(String.append(a, b)) : Bool}