def aes_nat_eq_step

qasim-bend-kit@0.1.0.2 · libs/AES256GCM.bend:312

import Base

312def aes_nat_eq_step(+a: Nat, +b: Nat,
313                    result: Maybe<&0, {a == b : Nat}>) -> Maybe<&0, {1n+a == 1n+b : Nat}>:
314    match result:
315        case None{}: None{}
316        case Some{proof}: Some{Equal.cong(Nat, Nat, n => 1n+n, a, b, proof)}