134   FUN_REL_syn (infixr "===>" 55)

   134   FUN_REL_syn (infixr "===>" 55)

   135 where

   135 where

   136   "E1 ===> E2 \<equiv> FUN_REL E1 E2"

   136   "E1 ===> E2 \<equiv> FUN_REL E1 E2"

   137 

   137 

   138 lemma FUN_REL_EQ:

   138 lemma FUN_REL_EQ:

   140 by (simp add: expand_fun_eq)

   140 by (simp add: expand_fun_eq)

   141 

   141 

   142 lemma FUN_QUOTIENT:

   142 lemma FUN_QUOTIENT:

   143   assumes q1: "QUOTIENT R1 abs1 rep1"

   143   assumes q1: "QUOTIENT R1 abs1 rep1"

   144   and     q2: "QUOTIENT R2 abs2 rep2"

   144   and     q2: "QUOTIENT R2 abs2 rep2"