def off.no

import bend-osdev-bytes@0.1.1.0/PROOF.bend as PROOF

import Base

773def off.no(-A: Type, h: {False{} == True{} : Bool}) -> A:
774  off.absurd(A, off.clash(h))

Uses (3)