def nat_encode

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

import Base

80def nat_encode(+a: Nat, +b: Nat, proof: {a == b : Nat}) -> nat_code(a, b):
81    %proof : nat_code(a, _)
82    nat_code_refl(a)