Definition. id_eq
id X = {t | ∃x. x ∈ X ∧ t = (x, x)}