def nat_decode_refl

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

import Base

93def nat_decode_refl(+a: Nat) ->
94    {nat_decode(a, a, nat_code_refl(a)) == {==} : {a == a : Nat}}:
95    match a:
96        case 0n: {==}
97        case 1n+p:
98            %Equal.sym({p == p : Nat},
99                nat_decode(p, p, nat_code_refl(p)), {==},
100                nat_decode_refl(p)) :
101                {Equal.cong(Nat, Nat, value => 1n+value, p, p, _) == {==} :
102                    {1n+p == 1n+p : Nat}}
103            {==}