law is_empty_append

bend-mathlib@0.8.1.0 · string.bend:398

import Base

398# An append is empty exactly when both parts are.
399law is_empty_append:
400  for a: String
401  for -b: String
402  {String.is_empty(String.append(a, b)) == Bool.and(String.is_empty(a), String.is_empty(b)) : Bool}