AESConstructorProof.key_certificates: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_ConstructorProof.bend as AESConstructorProof
Lines 6-26 of qasim-bend-kit@0.1.0.2/proof/AES_ConstructorProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_ConstructorProof.bend&start_line=6&end_line=26

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_CertificateProof.bend as Certificate

def key_certificates(+bytes: List<&2, U32>,
    +first_size: {List.length(&2, U32, bytes) == 32n : Nat},
    +first_valid: {AES.bytes_valid(bytes) == True{} : Bool},
    +second_size: {List.length(&2, U32, bytes) == 32n : Nat},
    +second_valid: {AES.bytes_valid(bytes) == True{} : Bool}) ->
    {AES.SecretKey{bytes, first_size, first_valid} ==
     AES.SecretKey{bytes, second_size, second_valid} : AES.SecretKey}:
    Equal.trans(AES.SecretKey,
        AES.SecretKey{bytes, first_size, first_valid},
        AES.SecretKey{bytes, second_size, first_valid},
        AES.SecretKey{bytes, second_size, second_valid},
        Equal.cong({List.length(&2, U32, bytes) == 32n : Nat}, AES.SecretKey,
            proof => AES.SecretKey{bytes, proof, first_valid},
            first_size, second_size,
            Certificate.nat_unique(List.length(&2, U32, bytes), 32n,
                first_size, second_size)),
        Equal.cong({AES.bytes_valid(bytes) == True{} : Bool}, AES.SecretKey,
            proof => AES.SecretKey{bytes, second_size, proof},
            first_valid, second_valid,
            Certificate.bool_unique(AES.bytes_valid(bytes), True{},
                first_valid, second_valid)))

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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.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=U32
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=SecretKey
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=bytes_valid
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=bool_unique
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=nat_unique