def nat_decode_encode

qasim-bend-kit@0.1.0.2 · proof/AES_CertificateProof.bend:105

import Base

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