def sp.absurd

bend-osdev-cbc@0.1.0.0 · PROOF.bend:103

import Base

103def sp.absurd(p: Nat, h: {1n+p == 0n : Nat}) -> Empty:
104  %h : sp.disc(_)
105  Unit{}