def absurd.sn_nat
import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOFimport Base
835def absurd.sn_nat(-k: Nat, e: {Some{k} == None{} : Maybe<&2, Nat>}) -> Empty:
836 absurd.sn(k, e)
Uses (4)
Used by (0)
No other definition uses this definition.
import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOFimport Base
835def absurd.sn_nat(-k: Nat, e: {Some{k} == None{} : Maybe<&2, Nat>}) -> Empty:
836 absurd.sn(k, e)
No other definition uses this definition.