1047   \end{itemize}

  1047   \end{itemize}

  1048 

  1048 

  1049   We defined the theorem @{text "inj_thm"} in such a way that

  1049   We defined the theorem @{text "inj_thm"} in such a way that

  1050   establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be

  1050   establishing the equivalence @{text "inj_thm \<longleftrightarrow> quot_thm"} can be

  1051   achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient

  1051   achieved by rewriting @{text "inj_thm"} with the preservation theorems and quotient

  1053   are used to fold the @{term Rep} with the raw constants. Next for

  1053   are used to fold the @{term Rep} with the raw constants. Next for

  1054   all abstractions and quantifiers the lambda and

  1054   all abstractions and quantifiers the lambda and

  1055   quantifier preservation theorems are used to replace the

  1055   quantifier preservation theorems are used to replace the

  1056   variables that include raw types with respects by quantifiers

  1056   variables that include raw types with respects by quantifiers

  1057   over variables that include quotient types. We show here only

  1057   over variables that include quotient types. We show here only