def reverse_source_suffix

qasim-bend-kit@0.1.0.2 · proof/JSON_SourceProof.bend:362

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

362def reverse_source_suffix(+value: J.Value,
363                          +members: Bool,
364                          +suffix: List<&2, J.Lexeme>) -> {List.reverse(&2, J.Lexeme, J.source(value, members, suffix)) == List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, suffix), List.reverse(&2, J.Lexeme, J.source(value, members, Nil{}))) : List<&2, J.Lexeme>}:
365    Equal.trans(List<&2, J.Lexeme>,
366        List.reverse(&2, J.Lexeme, J.source(value, members, suffix)),
367        List.reverse(&2, J.Lexeme, List.append(&2, J.Lexeme, J.source(value, members, Nil{}), suffix)),
368        List.append(&2, J.Lexeme, List.reverse(&2, J.Lexeme, suffix),
369            List.reverse(&2, J.Lexeme, J.source(value, members, Nil{}))),
370        Equal.cong(List<&2, J.Lexeme>, List<&2, J.Lexeme>, items => List.reverse(&2, J.Lexeme, items),
371            J.source(value, members, suffix),
372            List.append(&2, J.Lexeme, J.source(value, members, Nil{}), suffix),
373            source_append(value, members, Nil{}, suffix)),
374        LP.reverse_append(J.Lexeme, J.source(value, members, Nil{}), suffix))