Definition. inv_eq
inv f = {t | ∃x. ∃y. t = (y, x) ∧ (x, y) ∈ f}