388   and     q2: "QUOTIENT R2 Abs2 Rep2"

   388   and     q2: "QUOTIENT R2 Abs2 Rep2"

   389   and     a: "(R1 ===> R2) f g" "R1 x y"

   389   and     a: "(R1 ===> R2) f g" "R1 x y"

   390   shows "R2 (f x) (g y)"

   390   shows "R2 (f x) (g y)"

   391 using a by (rule FUN_REL_IMP)

   391 using a by (rule FUN_REL_IMP)

   392 

   392 

   393 

   398 

   394 (* combinators: I, K, o, C, W *)

   399 (* combinators: I, K, o, C, W *)

   395 

   400 

   396 lemma I_PRS:

   401 lemma I_PRS:

   397   assumes q: "QUOTIENT R Abs Rep"

   402   assumes q: "QUOTIENT R Abs Rep"