def bq.sz

bend-osdev-algo@0.1.0.0 · proof_bsearch.bend:141

import Base

141def bq.sz(-k: Nat, e: {1n+k == 0n : Nat}) -> Empty:
142  %Equal.sym(Nat, 1n+k, 0n, e) : bq.nt(_)
143  Unit{}