AESCertificateProof.nat_decode_refl: 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 93-103 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=93&end_line=103

import Base

def nat_decode_refl(+a: Nat) ->
    {nat_decode(a, a, nat_code_refl(a)) == {==} : {a == a : Nat}}:
    match a:
        case 0n: {==}
        case 1n+p:
            %Equal.sym({p == p : Nat},
                nat_decode(p, p, nat_code_refl(p)), {==},
                nat_decode_refl(p)) :
                {Equal.cong(Nat, Nat, value => 1n+value, p, p, _) == {==} :
                    {1n+p == 1n+p : Nat}}
            {==}

Uses (5):
  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=Nat
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=nat_code_refl
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/proof/AES_CertificateProof.bend&name=nat_decode