I have omitted the requirement that $\tau $ be substitutable for $x$ in $\phi$ since it makes the statement of the rule more complicated and plays no rôle in the point I am making here.

-- ShaughanLavine - 16 Mar 2005