Definition. choice_function_equi
choice_function f ↔ function f ∧ ∀x. x ∈ dom f → app f x ∈ x