~~ package:rebase

Group subtraction: x ~~ y == x <> invert y
Kind heterogeneous propositional equality. Like :~:, a :~~: b is inhabited by a terminating value if and only if a is the same type as b.