JSONStringProof.append_assoc: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend as JSONStringProof
Lines 11-15 of qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&start_line=11&end_line=15

import Base

def append_assoc(+a: String, +b: String, +c: String) -> {(a ++ b) ++ c == a ++ (b ++ c) : String}:
    match a:
        case SNil{}: {==}
        case SCon{h, t}:
            Equal.cong(String, String, s => SCon{h, s}, (t ++ b) ++ c, t ++ (b ++ c), append_assoc(t, b, c))

Uses (3):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.append