def aes_nat_eq_self

qasim-bend-kit@0.1.0.2 · proof/AES_EnvelopeProof.bend:695

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

695def aes_nat_eq_self(+n: Nat) ->
696    {AES.aes_nat_eq_proof(n, n) == Some{{==}} :
697        Maybe<&0, {n == n : Nat}>}:
698    match n:
699        case 0n: {==}
700        case 1n+p:
701            Equal.cong(Maybe<&0, {p == p : Nat}>,
702                Maybe<&0, {1n+p == 1n+p : Nat}>,
703                result => AES.aes_nat_eq_step(p, p, result),
704                AES.aes_nat_eq_proof(p, p), Some{{==}},
705                aes_nat_eq_self(p))