Description: Extend wff definition to include the redundancy operator for propositions.
wff redund ( ph , ps , ch )