def absurd.ns

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

import Base

54def absurd.ns(-k: Nat, e: {None{} == Some{k} : Maybe<&2, Nat>}) -> Empty:
55  %Equal.sym(Maybe<&2, Nat>, None{}, Some{k}, e) : absurd.maybe(_)
56  Unit{}