Description: Extend wff definition to include proper substitution (read "the wff that results when y is properly substituted for x in wff ph "). (Contributed by NM, 24-Jan-2006)