RESQ_REWR_CANON : thm -> thm
STRUCTURE
SYNOPSIS
Transform a theorem into a form accepted for rewriting.
DESCRIPTION
RESQ_REWR_CANON transforms a theorem into a form accepted by COND_REWR_TAC. The input theorem should be headed by a series of restricted universal quantifications in the following form
   !x1::P1. ... !xn::Pn. u[xi] = v[xi])
Other variables occurring in u and v may be universally quantified. The output theorem will have all ordinary universal quantifications moved to the outer most level with possible renaming to prevent variable capture, and have all restricted universal quantifications converted to implications. The output theorem will be in the form accepted by COND_REWR_TAC.
FAILURE
This function fails is the input theorem is not in the correct form.

SEEALSO
HOL  Trindemossen-1