def bits.absurd

bend-osdev-caps@0.1.0.0 · PROOF.bend:43

import Base

43def bits.absurd(-x: Bool, +e: {False{} == True{} : Bool}) -> {x == True{} : Bool}:
44  Empty.absurd({x == True{} : Bool}, bits.ft(e))