def sp.absurd

bend-osdev-cipher-modes@0.1.0.0 · PROOF.bend:148

import Base

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