def bits.absurd_eq

import bend-osdev-caps@0.1.0.0/PROOF.bend as PROOF

import Base

46def bits.absurd_eq(-T: Type, -x: T, -y: T, +e: {False{} == True{} : Bool}) -> {x == y : T}:
47  Empty.absurd({x == y : T}, bits.ft(e))

Uses (3)