530 text {* Preservation of quantifiers, abstractions, relations, quotient-constants

   530 text {*

   531   (definitions) and user given constant preservation lemmas *}

   531   The @{text REG} and @{text INJ} functions have been defined in such a way

   532   that establishing the goal theorem now consists only on rewriting the

   533   injected theorem with the preservation theorems.

   534 

   535   \begin{itemize}

   536   \item First for lifted constants, their definitions are the preservation rules for

   537     them.

   538   \item For lambda abstractions lambda preservation establishes

   539     the equality between the injected theorem and the goal. This allows both

   540     abstraction and quantification over lifted types.

   541     @{thm [display] lambda_prs[no_vars]}

   542   \item Relations over lifted types are folded with:

   543     @{thm [display] Quotient_rel_rep[no_vars]}

   544   \item User given preservation theorems, that allow using higher level operations

   545     and containers of types being lifted. An example may be

   546     @{thm [display] map_prs(1)[no_vars]}

   547   \end{itemize}

   548 

   549  Preservation of relations and user given constant preservation lemmas *}