Definition. relation_equi
relation R ↔ ∀t. t ∈ R → ∃x. ∃y. t = (x, y)