JSONRenderLexProof.field_text: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend as JSONRenderLexProof
Lines 309-327 of qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_RenderLexProof.bend&start_line=309&end_line=327

import Base
import qasim-bend-kit@0.1.0.2/libs/JSON.bend as J
import qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend as S

def field_text(+key: String,
               +text: String) -> {J.render_object_field(SNil{}, key, text) == ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text) : String}:
    Equal.trans(String,
        J.render_object_field(SNil{}, key, text),
        SCon{'"', J.escape_string(key) ++ ("\":" ++ text)},
        ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text),
        Equal.cong(String, String,
            x => SCon{'"', x},
            (J.escape_string(key) ++ "\":") ++ text,
            J.escape_string(key) ++ ("\":" ++ text),
            S.append_assoc(J.escape_string(key), "\":", text)),
        Equal.sym(String,
            ("\"" ++ J.escape_string(key) ++ "\"") ++ (":" ++ text),
            SCon{'"', J.escape_string(key) ++ ("\":" ++ text)},
            Equal.cong(String, String,
                x => SCon{'"', x},
                (J.escape_string(key) ++ "\"") ++ (":" ++ text),
                J.escape_string(key) ++ ("\"" ++ (":" ++ text)),
                S.append_assoc(J.escape_string(key), "\"", ":" ++ text))))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Char
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=escape_string
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=render_object_field
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_StringProof.bend&name=append_assoc