standardize the notation of function application
add the definition of reducibility candidate
add a notation for tyfun