AESCertificateProof.nat_decode_encode: def of qasim-bend-kit@0.1.0.2
Import: import qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend as AESCertificateProof
Lines 105-109 of qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend: https://jend.leeeet.dev/read.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&start_line=105&end_line=109

import Base

def nat_decode_encode(+a: Nat, +b: Nat, +proof: {a == b : Nat}) ->
    {nat_decode(a, b, nat_encode(a, b, proof)) == proof : {a == b : Nat}}:
    %path@proof : {nat_decode(a, _, nat_encode(a, _, path)) == path :
        {a == _ : Nat}}
    nat_decode_refl(a)

Uses (4):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=nat_decode
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=nat_decode_refl
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=nat_encode