Description: Extend the definition of a wff to include the function predicate with a domain. (Read: A is a function on B .)
wff A Fn B