def ns.sz

bend-osdev-word64@0.1.1.0 · proof_shift.bend:33

import Base

33def ns.sz(-a: Nat, e: {1n+a == 0n : Nat}) -> Empty:
34  %e : ns.nd(_)
35  Unit{}