AESLengthLimitProof.length_limit_go_same: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend as AESLengthLimitProof
Lines 22-69 of qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend&start_line=22&end_line=69

import Base
import qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend as AES
import qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend as ZipLengthProof

def length_limit_go_same(+a: List<&2, U32>, +b: List<&2, U32>,
    +low: U32, +high: U32, +max_low: U32, +max_high: U32,
    +within: Bool,
    same_length: {List.length(&2, U32, a) ==
        List.length(&2, U32, b) : Nat}) ->
    {AES.bytes_length_limit.go(List.length(&2, U32, a), a,
        low, high, max_low, max_high, within) ==
     AES.bytes_length_limit.go(List.length(&2, U32, b), b,
        low, high, max_low, max_high, within) : Bool}:
    match a b within:
        case Nil{} Nil{} _: {==}
        case Nil{} y <> ys _:
            mismatch = Equal.cong(Nat, Bool,
                n => Nat.is_eq(0n, n),
                List.length(&2, U32, Nil{}),
                List.length(&2, U32, y <> ys), same_length)
            Empty.absurd(
                {AES.bytes_length_limit.go(0n, Nil{}, low, high,
                    max_low, max_high, within) ==
                 AES.bytes_length_limit.go(
                    List.length(&2, U32, y <> ys), y <> ys,
                    low, high, max_low, max_high, within) : Bool},
                ZipLengthProof.false_true(Equal.sym(Bool,
                    True{}, False{}, mismatch)))
        case x <> xs Nil{} _:
            mismatch = Equal.cong(Nat, Bool,
                n => Nat.is_eq(n, 0n),
                List.length(&2, U32, x <> xs),
                List.length(&2, U32, Nil{}), same_length)
            Empty.absurd(
                {AES.bytes_length_limit.go(
                    List.length(&2, U32, x <> xs), x <> xs,
                    low, high, max_low, max_high, within) ==
                 AES.bytes_length_limit.go(0n, Nil{}, low, high,
                    max_low, max_high, within) : Bool},
                ZipLengthProof.false_true(mismatch))
        case x <> xs y <> ys False{}: {==}
        case x <> xs y <> ys True{}:
            tail_length = Equal.cong(Nat, Nat, predecessor,
                List.length(&2, U32, x <> xs),
                List.length(&2, U32, y <> ys), same_length)
            +next_low = U32.add(low, 1)
            +next_high = Bool.pick(U32, U32.is_eq(next_low, 0),
                U32.add(high, 1), high)
            next_within = AES.length_pair_within(next_low, next_high,
                max_low, max_high)
            length_limit_go_same(xs, ys, next_low, next_high,
                max_low, max_high, next_within, tail_length)

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=Bool.pick
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Empty.absurd
  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=List
  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.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=bytes_length_limit.go
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=length_pair_within
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_LengthLimitProof.bend&name=predecessor
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ZipLengthProof.bend&name=false_true