Definition. num_eq_equi
num_eq X Y ↔ ∃f. bij f X Y