QCONV
Conv.QCONV : conv -> conv
Stops a conversion raising the UNCHANGED exception.
If conversion c applied to term t raises the UNCHANGED exception,
then QCONV c t instead returns the theorem |- t = t.
Failure
QCONV c t fails if the application of c to t fails.