JSONSourceProof.nested_render_append: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend as JSONSourceProof
Lines 32-47 of qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&start_line=32&end_line=47

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

def nested_render_append(+outer: J.Value,
                         +inner: J.Value,
                         +inner_members: Bool,
                         +prefix: String,
                         +suffix: String,
                         +outer_append: {J.render(outer, False{}, J.render(inner, inner_members, prefix)) ++ suffix == J.render(outer, False{}, J.render(inner, inner_members, prefix) ++ suffix) : String},
                         +inner_append: {J.render(inner, inner_members, prefix) ++ suffix == J.render(inner, inner_members, prefix ++ suffix) : String}) -> {J.render(outer, False{}, J.render(inner, inner_members, prefix)) ++ suffix == J.render(outer, False{}, J.render(inner, inner_members, prefix ++ suffix)) : String}:
    Equal.trans(String,
        J.render(outer, False{}, J.render(inner, inner_members, prefix)) ++ suffix,
        J.render(outer, False{}, J.render(inner, inner_members, prefix) ++ suffix),
        J.render(outer, False{}, J.render(inner, inner_members, prefix ++ suffix)),
        outer_append,
        Equal.cong(String, String, text => J.render(outer, False{}, text),
            J.render(inner, inner_members, prefix) ++ suffix,
            J.render(inner, inner_members, prefix ++ suffix),
            inner_append))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.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=Value
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=render