law nil_append
import bend-mathlib@0.8.1.0/string.bend as Stringimport Base
27# The empty string is a left identity for append: "" ++ a = a.
28law nil_append:
29 for -a: String
30 {String.append(SNil{}, a) == a : String}
import bend-mathlib@0.8.1.0/string.bend as Stringimport Base
27# The empty string is a left identity for append: "" ++ a = a.
28law nil_append:
29 for -a: String
30 {String.append(SNil{}, a) == a : String}