AESEnvelopeProof.aes_nat_eq_self: 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 695-705 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=695&end_line=705

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

def aes_nat_eq_self(+n: Nat) ->
    {AES.aes_nat_eq_proof(n, n) == Some{{==}} :
        Maybe<&0, {n == n : Nat}>}:
    match n:
        case 0n: {==}
        case 1n+p:
            Equal.cong(Maybe<&0, {p == p : Nat}>,
                Maybe<&0, {1n+p == 1n+p : Nat}>,
                result => AES.aes_nat_eq_step(p, p, result),
                AES.aes_nat_eq_proof(p, p), Some{{==}},
                aes_nat_eq_self(p))

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=Maybe
  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/libs/AES256GCM.bend&name=aes_nat_eq_proof
  https://jend.leeeet.dev/definition.txt?path=qasim-bend-kit@0.1.0.2/libs/AES256GCM.bend&name=aes_nat_eq_step