def absurd.ns32

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

import Base

821def absurd.ns32(-k: U32, e: {None{} == Some{k} : Maybe<&2, U32>}) -> Empty:
822  %Equal.sym(Maybe<&2, U32>, None{}, Some{k}, e) : absurd.maybe32(_)
823  Unit{}