JSONListProof.reverse_cons: 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 36-39 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=36&end_line=39

import Base

def reverse_cons(-A: Data,
                 +head: A,
                 +tail: List<&2, A>) -> {List.reverse(&2, A, head <> tail) == List.append(&2, A, List.reverse(&2, A, tail), head <> Nil{}) : List<&2, A>}:
    reverse_go_append(A, tail, Nil{}, head <> Nil{})

Uses (4):
  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=reverse_go_append