JSONListProof.reverse_append: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend as JSONListProof
Lines 41-74 of qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend&start_line=41&end_line=74

import Base

def reverse_append(-A: Data,
                   +xs: List<&2, A>,
                   +ys: List<&2, A>) -> {List.reverse(&2, A, List.append(&2, A, xs, ys)) == List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, xs)) : List<&2, A>}:
    match xs:
        case Nil{}:
            Equal.sym(List<&2, A>, List.append(&2, A, List.reverse(&2, A, ys), Nil{}),
                List.reverse(&2, A, ys),
                append_nil(A, List.reverse(&2, A, ys)))
        case h <> t:
            Equal.trans(List<&2, A>,
                List.reverse(&2, A, List.append(&2, A, h <> t, ys)),
                List.append(&2, A, List.reverse(&2, A, List.append(&2, A, t, ys)), h <> Nil{}),
                List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, h <> t)),
                reverse_go_append(A, List.append(&2, A, t, ys), Nil{}, h <> Nil{}),
                Equal.trans(List<&2, A>,
                    List.append(&2, A, List.reverse(&2, A, List.append(&2, A, t, ys)), h <> Nil{}),
                    List.append(&2, A, List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, t)), h <> Nil{}),
                    List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, h <> t)),
                    Equal.cong(List<&2, A>, List<&2, A>, xs => List.append(&2, A, xs, h <> Nil{}),
                        List.reverse(&2, A, List.append(&2, A, t, ys)),
                        List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, t)),
                        reverse_append(A, t, ys)),
                    Equal.trans(List<&2, A>,
                        List.append(&2, A, List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, t)), h <> Nil{}),
                        List.append(&2, A, List.reverse(&2, A, ys), List.append(&2, A, List.reverse(&2, A, t), h <> Nil{})),
                        List.append(&2, A, List.reverse(&2, A, ys), List.reverse(&2, A, h <> t)),
                        append_assoc(A, List.reverse(&2, A, ys), List.reverse(&2, A, t), h <> Nil{}),
                        Equal.cong(List<&2, A>, List<&2, A>, xs => List.append(&2, A, List.reverse(&2, A, ys), xs),
                            List.append(&2, A, List.reverse(&2, A, t), h <> Nil{}),
                            List.reverse(&2, A, h <> t),
                            Equal.sym(List<&2, A>,
                                List.reverse(&2, A, h <> t),
                                List.append(&2, A, List.reverse(&2, A, t), h <> Nil{}),
                                reverse_go_append(A, t, Nil{}, h <> Nil{}))))))

Uses (9):
  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=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=qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend&name=append_assoc
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend&name=append_nil
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/JSON_ListProof.bend&name=reverse_go_append