def un.sz

bend-osdev-u32@0.1.0.0 · PROOF.bend:1030

import Base

1030def un.sz(-a: Nat, e: {1n+a == 0n : Nat}) -> Empty:
1031  %e : un.nz(_)
1032  Unit{}