law nil_append_sym

bend-mathlib@0.8.1.0 · string.bend:540

import Base

540# The empty string is a left identity for append: "" ++ a = a, reversed to rewrite toward the simple side.
541law nil_append_sym:
542  for -a: String
543  {a == String.append(SNil{}, a) : String}