def absurd.sn

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

import Base

50def absurd.sn(-k: Nat, e: {Some{k} == None{} : Maybe<&2, Nat>}) -> Empty:
51  %e : absurd.maybe(_)
52  Unit{}