AESIdentityProof.fixed_hex_equal: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend as AESIdentityProof
Lines 89-101 of qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_IdentityProof.bend&start_line=89&end_line=101

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_EnvelopeProof.bend as Encoding

def fixed_hex_equal(+n: Nat, +first: List<&2, U32>, +second: List<&2, U32>,
    first_size: {List.length(&2, U32, first) == n : Nat},
    second_size: {List.length(&2, U32, second) == n : Nat},
    same: {AES.hex_bytes(AES.fixed_bytes(n, first)) == AES.hex_bytes(AES.fixed_bytes(n, second)) : String}) ->
    {AES.hex_bytes(first) == AES.hex_bytes(second) : String}:
    first_path = Equal.cong(List<&2, U32>, String, bytes => AES.hex_bytes(bytes),
        AES.fixed_bytes(n, first), first, Encoding.aes_fixed_bytes_identity(n, first, first_size))
    second_path = Equal.cong(List<&2, U32>, String, bytes => AES.hex_bytes(bytes),
        AES.fixed_bytes(n, second), second, Encoding.aes_fixed_bytes_identity(n, second, second_size))
    Equal.trans(String, AES.hex_bytes(first), AES.hex_bytes(AES.fixed_bytes(n, first)), AES.hex_bytes(second),
        Equal.sym(String, AES.hex_bytes(AES.fixed_bytes(n, first)), AES.hex_bytes(first), first_path),
        Equal.trans(String, AES.hex_bytes(AES.fixed_bytes(n, first)), AES.hex_bytes(AES.fixed_bytes(n, second)),
            AES.hex_bytes(second), same, second_path))

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