Theorem choice_fn_unfold

Proof
01. 1 ⊢ choice_function f, hypo.
02. 1 ⊢ function f ∧ ∀x. x ∈ dom f → app f x ∈ x,
  lsubj_elim choice_function_equi 1.
choice_fn_unfold. ⊢ choice_function f →
  function f ∧ ∀x. x ∈ dom f → app f x ∈ x, subj_intro 2.