def AP.sz

bend-osdev-array@0.1.0.1 · PROOF.bend:41

import Base

41# 1 + k is never 0
42def AP.sz(-k: Nat, e: {1n+k == 0n : Nat}) -> Empty:
43  %Equal.sym(Nat, 1n+k, 0n, e) : AP.nat_t(_)
44  Unit{}