117 theorem msgrel_imp_eq_freediscrim:

   117 theorem msgrel_imp_eq_freediscrim:

   118   assumes a: "U \<sim> V"

   118   assumes a: "U \<sim> V"

   119   shows "freediscrim U = freediscrim V"

   119   shows "freediscrim U = freediscrim V"

   120 using a by (induct, auto)

   120 using a by (induct, auto)

   121 

   121 

   123 subsection{*The Initial Algebra: A Quotiented Message Type*}

   122 subsection{*The Initial Algebra: A Quotiented Message Type*}

   124 

   123 

   125 quotient  msg = freemsg / msgrel

   124 quotient  msg = freemsg / msgrel

   126   by (rule equiv_msgrel)

   125   by (rule equiv_msgrel)

   127 

   126