Description: Corollary of dtru . This example illustrates the danger of blindly
trusting the standard Deduction Theorem without accounting for free
variables: the theorem form of this deduction is not valid, as shown by
dtrucor2 . (Contributed by NM, 27-Jun-2002)