AESEnvelopeProof.aes_fixed_bytes_length: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend as AESEnvelopeProof
Lines 542-553 of qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_EnvelopeProof.bend&start_line=542&end_line=553

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

def aes_fixed_bytes_length(+n: Nat, +bytes: List<&2, U32>) ->
    {List.length(&2, U32, AES.fixed_bytes(n, bytes)) == n : Nat}:
    match n bytes:
        case 0n _: {==}
        case 1n+p Nil{}:
            Equal.cong(Nat, Nat, x => 1n+x,
                List.length(&2, U32, AES.fixed_bytes(p, Nil{})), p,
                aes_fixed_bytes_length(p, Nil{}))
        case 1n+p byte <> tail:
            Equal.cong(Nat, Nat, x => 1n+x,
                List.length(&2, U32, AES.fixed_bytes(p, tail)), p,
                aes_fixed_bytes_length(p, tail))

Uses (6):
  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.length
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=fixed_bytes