Function choice_function_realization_ty 

pub fn choice_function_realization_ty() -> Expr

ChoiceFunctionRealization : (Nat → Prop) → (Nat → Nat) Realizing a choice function from a provability assumption.