701   "\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of

   701   "\<alpha>"}-equated lambda terms. Homeier formulates the restrictions in terms of

   702   the properties of \emph{respectfulness} and \emph{preservation}. We have

   702   the properties of \emph{respectfulness} and \emph{preservation}. We have

   703   to slightly extend Homeier's definitions in order to deal with quotient

   703   to slightly extend Homeier's definitions in order to deal with quotient

   704   compositions. 

   704   compositions. 

   705 

   705 

   706   To formally define what respectfulness is, we have to first define 

   709   To formally define what respectfulness is, we have to first define 

   707   the notion of \emph{aggregate equivalence relations} using the function @{text "REL(\<sigma>, \<tau>)"}

   710   the notion of \emph{aggregate equivalence relations} using the function @{text "REL(\<sigma>, \<tau>)"}

   708   The idea behind this function is to simultaneously descend into the raw types

   711   The idea behind this function is to simultaneously descend into the raw types

   709   @{text \<sigma>} and quotient types @{text \<tau>}, and generate the appropriate

   712   @{text \<sigma>} and quotient types @{text \<tau>}, and generate the appropriate

   710   quotient equivalence relations in places where the types differ and equalities

   713   quotient equivalence relations in places where the types differ and equalities

   841 

   844 

   842 section {* Lifting of Theorems\label{sec:lift} *}

   845 section {* Lifting of Theorems\label{sec:lift} *}

   843 

   846 

   844 text {*

   847 text {*

   845 

   848 

   846   The main benefit of a quotient package is to lift automatically theorems over raw

   855   The main benefit of a quotient package is to lift automatically theorems over raw

   847   types to theorems over quotient types. We will perform this lifting in

   856   types to theorems over quotient types. We will perform this lifting in

   848   three phases, called \emph{regularization},

   857   three phases, called \emph{regularization},

   849   \emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.

   858   \emph{injection} and \emph{cleaning} according to procedures in Homeier's ML-code.

   850 

   859 

  1194   only exist in \cite{Homeier05} as ML-code, not included in the paper.

  1203   only exist in \cite{Homeier05} as ML-code, not included in the paper.

  1195   Like Homeier's, our quotient package can deal with partial equivalence

  1204   Like Homeier's, our quotient package can deal with partial equivalence

  1196   relations, but for lack of space we do not describe the mechanisms

  1205   relations, but for lack of space we do not describe the mechanisms

  1197   needed for this kind of quotient constructions.

  1206   needed for this kind of quotient constructions.

  1198 

  1207 

  1199 

  1210 

  1200   One feature of our quotient package is that when lifting theorems, the user

  1211   One feature of our quotient package is that when lifting theorems, the user

  1201   can precisely specify what the lifted theorem should look like. This feature

  1212   can precisely specify what the lifted theorem should look like. This feature

  1202   is necessary, for example, when lifting an induction principle for two

  1213   is necessary, for example, when lifting an induction principle for two

  1203   lists.  Assuming this principle has as the conclusion a predicate of the

  1214   lists.  Assuming this principle has as the conclusion a predicate of the