JSONStringProof.append_nil: 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 5-9 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=5&end_line=9

import Base

def append_nil(+text: String) -> {text ++ SNil{} == text : String}:
    match text:
        case SNil{}: {==}
        case SCon{h, t}:
            Equal.cong(String, String, s => SCon{h, s}, t ++ SNil{}, t, append_nil(t))

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