JSONSourceProof.reverse_source_object_members_after_separator: 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 462-474 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=462&end_line=474

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_ListProof.bend as LP

def reverse_source_object_members_after_separator(+key: String,
                                                  +value: J.Value,
                                                  +tail: List<&2, Sigma<&2, &2, String, key => J.Value>>) -> {reverse_source_task(J.Obj{(key, value) <> tail}, RenderMembers{}) == List.append(&2, J.Lexeme, reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}), J.Punctuation{','} <> Nil{}) : List<&2, J.Lexeme>}:
    Equal.trans(List<&2, J.Lexeme>,
        reverse_source_task(J.Obj{(key, value) <> tail}, RenderMembers{}),
        List.reverse(&2, J.Lexeme, J.Punctuation{','} <> source_after_separator(J.Obj{(key, value) <> tail}, Nil{})),
        List.append(&2, J.Lexeme, reverse_source_task(J.Obj{(key, value) <> tail}, RenderAfterSeparator{}),
            J.Punctuation{','} <> Nil{}),
        Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items),
            J.source(J.Obj{(key, value) <> tail}, True{}, Nil{}),
            J.Punctuation{','} <> source_after_separator(J.Obj{(key, value) <> tail}, Nil{}),
            {==}),
        LP.reverse_cons(J.Lexeme, J.Punctuation{','}, source_after_separator(J.Obj{(key, value) <> tail}, Nil{})))

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.append
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List.reverse
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=String
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/JSON.bend&name=Lexeme
  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=source
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend&name=reverse_cons
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=RenderMode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=reverse_source_task
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_SourceProof.bend&name=source_after_separator