298 

   299   To lift theorems that talk about insertion in lists of lifted types

   300   we need to know that for any quotient type with the abstraction and

   301   representation functions @{text "Abs"} and @{text Rep} we have:

   302 

   303   @{thm [display] (concl) cons_prs[no_vars]}

   304 

   305   This is not enough to lift theorems that talk about quotient compositions.

   306   For some constants (for example empty list) it is possible to show a

   307   general compositional theorem, but for @{term "op #"} it is necessary

   308   to show that it respects the particular quotient type:

   309 

   310   @{thm [display] insert_preserve2[no_vars]}