AESZipLengthProof.append_length: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend as AESZipLengthProof
Lines 116-126 of qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&start_line=116&end_line=126

import Base

def append_length(+xs: List<&2, U32>, +ys: List<&2, U32>) ->
    {List.length(&2, U32, List.append(&2, U32, xs, ys)) ==
     Nat.add(List.length(&2, U32, xs), List.length(&2, U32, ys)) : Nat}:
    match xs:
        case Nil{}: {==}
        case x <> tail:
            Equal.cong(Nat, Nat, n => 1n+n,
                List.length(&2, U32, List.append(&2, U32, tail, ys)),
                Nat.add(List.length(&2, U32, tail),
                    List.length(&2, U32, ys)),
                append_length(tail, ys))

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  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.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32