136 by (blast)

   136 by (blast)

   137 

   137 

   138 lemma QUOTIENT_PROD:

   138 lemma QUOTIENT_PROD:

   139   assumes a: "QUOTIENT E1 Abs1 Rep1"

   139   assumes a: "QUOTIENT E1 Abs1 Rep1"

   140   and     b: "QUOTIENT E2 Abs2 Rep2"

   140   and     b: "QUOTIENT E2 Abs2 Rep2"

   142 using a b unfolding QUOTIENT_def

   142 using a b unfolding QUOTIENT_def

   143 oops

   143 oops

   144 

   144 

   145 lemma QUOTIENT_ABS_REP_LIST:

   145 lemma QUOTIENT_ABS_REP_LIST:

   146   assumes a: "QUOTIENT_ABS_REP Abs Rep"

   146   assumes a: "QUOTIENT_ABS_REP Abs Rep"