def bits.absurd_tf

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

import Base

49def bits.absurd_tf(-T: Type, -x: T, -y: T, +e: {True{} == False{} : Bool}) -> {x == y : T}:
50  Empty.absurd({x == y : T}, bits.tf(e))

Uses (3)