def absurd.sz

bend-osdev-algo@0.1.0.0 · PROOF.bend:39

import Base

39def absurd.sz(-k: Nat, e: {1n+k == 0n : Nat}) -> Empty:
40  %e : absurd.nat(_)
41  Unit{}