def nat_code_refl

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

import Base

75def nat_code_refl(a: Nat) -> nat_code(a, a):
76    match a:
77        case 0n: Unit{}
78        case 1n+p: nat_code_refl(p)