JSONStringProof.reverse_go_append: 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 17-28 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=17&end_line=28

import Base

def reverse_go_append(+text: String,
                      +acc: String,
                      +suffix: String) -> {String.reverse.go(text, acc ++ suffix) == String.reverse.go(text, acc) ++ suffix : String}:
    match text:
        case SNil{}: {==}
        case SCon{head, tail}:
            Equal.trans(String,
                String.reverse.go(tail, SCon{head, acc ++ suffix}),
                String.reverse.go(tail, SCon{head, acc} ++ suffix),
                String.reverse.go(tail, SCon{head, acc}) ++ suffix,
                {==},
                reverse_go_append(tail, SCon{head, acc}, suffix))

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  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
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String.reverse.go