diff -r 5606de1e5034 -r d769c24094cf Quotient-Paper/Paper.thy
--- a/Quotient-Paper/Paper.thy	Fri Aug 27 16:00:19 2010 +0800
+++ b/Quotient-Paper/Paper.thy	Fri Aug 27 19:06:30 2010 +0800
@@ -16,10 +16,6 @@
   - explain how Quotient R Abs Rep is proved (j-version)
   - give an example where precise specification helps (core Haskell in nominal?)
 
-  - Quote from Peter:
-
-    One might think quotient have been studied to death, but
-
   - Mention Andreas Lochbiler in Acknowledgements and 'desceding'.
 
 *)
@@ -29,16 +25,17 @@
   pred_comp ("_ \<circ>\<circ> _" [1, 1] 30) and
   "op -->" (infix "\<longrightarrow>" 100) and
   "==>" (infix "\<Longrightarrow>" 100) and
-  fun_map ("_ \<^raw:\mbox{\singlearr}> _" 51) and
-  fun_rel ("_ \<^raw:\mbox{\doublearr}> _" 51) and
+  fun_map ("_ \<singlearr> _" 51) and
+  fun_rel ("_ \<doublearr> _" 51) and
   list_eq (infix "\<approx>" 50) and (* Not sure if we want this notation...? *)
   fempty ("\<emptyset>") and
   funion ("_ \<union> _") and
   finsert ("{_} \<union> _") and 
   Cons ("_::_") and
   concat ("flat") and
-  fconcat ("\<Union>")
- 
+  fconcat ("\<Union>") and
+  Quotient ("Quot _ _ _")
+
   
 
 ML {*
@@ -358,7 +355,8 @@
   we can get back to \eqref{adddef}. 
   In what follows we shall use the convention to write @{text "map_\<kappa>"} for a map-function 
   of the type-constructor @{text \<kappa>}. For a type @{text \<kappa>} with arguments @{text "\<alpha>\<^isub>1\<^isub>\<dots>\<^isub>n"} the
-  type of @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}. For example @{text "map_list"}
+  type of the function @{text "map_\<kappa>"} has to be @{text "\<alpha>\<^isub>1\<Rightarrow>\<dots>\<Rightarrow>\<alpha>\<^isub>n\<Rightarrow>\<alpha>\<^isub>1\<dots>\<alpha>\<^isub>n \<kappa>"}. 
+  For example @{text "map_list"}
   has to have the type @{text "\<alpha>\<Rightarrow>\<alpha> list"}.
   In our implementation we maintain
   a database of these map-functions that can be dynamically extended.
@@ -390,7 +388,7 @@
   An element @{text "x"} respects a relation @{text "R"} provided @{text "R x x"}.
   \end{definition}
 
-  \begin{definition}[Bounded Quantification and Bounded Abstractions]\label{def:babs}
+  \begin{definition}[Bounded $\forall$ and $\lambda$]\label{def:babs}
   @{text "\<forall>x \<in> S. P x"} holds if for all @{text x}, @{text "x \<in> S"} implies @{text "P x"};
   and @{text "(\<lambda>x \<in> S. f x) = f x"} provided @{text "x \<in> S"}.
   \end{definition}
@@ -402,28 +400,32 @@
   Given a relation $R$, an abstraction function $Abs$
   and a representation function $Rep$, the predicate @{term "Quotient R Abs Rep"}
   holds if and only if
-  \begin{enumerate}
-  \item @{thm (rhs1) Quotient_def[of "R", no_vars]}
-  \item @{thm (rhs2) Quotient_def[of "R", no_vars]}
-  \item @{thm (rhs3) Quotient_def[of "R", no_vars]}
-  \end{enumerate}
+  \begin{isabelle}\ \ \ \ \ %%%%
+  \begin{tabular}{rl}
+  (i) & \begin{isa}@{thm (rhs1) Quotient_def[of "R", no_vars]}\end{isa}\\
+  (ii) & \begin{isa}@{thm (rhs2) Quotient_def[of "R", no_vars]}\end{isa}\\
+  (iii) & \begin{isa}@{thm (rhs3) Quotient_def[of "R", no_vars]}\end{isa}\\
+  \end{tabular}
+  \end{isabelle}
   \end{definition}
 
   \noindent
-  The value of this definition lies in the fact that validity of @{text "Quotient R Abs Rep"} can 
-  often be proved in terms of the validity of @{text "Quotient"} over the constituent 
+  The value of this definition lies in the fact that validity of @{term "Quotient R Abs Rep"} can 
+  often be proved in terms of the validity of @{term "Quot"} over the constituent 
   types of @{text "R"}, @{text Abs} and @{text Rep}. 
   For example Homeier proves the following property for higher-order quotient
   types:
  
   \begin{proposition}\label{funquot}
+  \begin{isa}
   @{thm[mode=IfThen] fun_quotient[where ?R1.0="R\<^isub>1" and ?R2.0="R\<^isub>2" 
       and ?abs1.0="Abs\<^isub>1" and ?abs2.0="Abs\<^isub>2" and ?rep1.0="Rep\<^isub>1" and ?rep2.0="Rep\<^isub>2"]}
+  \end{isa}
   \end{proposition}
 
   \noindent
   As a result, Homeier is able to build an automatic prover that can nearly
-  always discharge a proof obligation involving @{text "Quotient"}. Our quotient
+  always discharge a proof obligation involving @{text "Quot"}. Our quotient
   package makes heavy 
   use of this part of Homeier's work including an extension 
   for dealing with compositions of equivalence relations defined as follows:
@@ -431,7 +433,7 @@
 %%% FIXME Referee 2 claims that composition-of-relations means OO, and this is also
 %%% what wikipedia says. Any idea for a different name? Conjugation of Relations?
 
-  \begin{definition}[Composition of Relations]
+  \begin{definition}%%[Composition of Relations]
   @{abbrev "rel_conj R\<^isub>1 R\<^isub>2"} where @{text "\<circ>\<circ>"} is the predicate
   composition defined by 
   @{thm (concl) pred_compI[of "R\<^isub>1" "x" "y" "R\<^isub>2" "z"]}
@@ -450,11 +452,15 @@
   with @{text R} being an equivalence relation, then
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{text  "Quotient (rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>) (Abs_fset \<circ> map_list Abs) (map_list Rep \<circ> Rep_fset)"}
+  \begin{tabular}{r@ {\hspace{1mm}}l}
+  @{text  "Quot"} & @{text "(rel_list R \<circ>\<circ>\<circ> \<approx>\<^bsub>list\<^esub>)"}\\
+                  & @{text "(Abs_fset \<circ> map_list Abs)"}\\ 
+                  & @{text "(map_list Rep \<circ> Rep_fset)"}\\
+  \end{tabular}
   \end{isabelle}
 *}
 
-section {* Quotient Types and Quotient Definitions\label{sec:type} *}
+section {* Quotient Types and Quotient\\ Definitions\label{sec:type} *}
 
 text {*
   The first step in a quotient construction is to take a name for the new
@@ -521,7 +527,7 @@
   (for the proof see \cite{Homeier05}).
 
   \begin{proposition}
-  @{text "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
+  @{term "Quotient R Abs_\<kappa>\<^isub>q Rep_\<kappa>\<^isub>q"}.
   \end{proposition}
 
   The next step in a quotient construction is to introduce definitions of new constants
@@ -568,20 +574,19 @@
   %
   \begin{center}
   \hfill
-  \begin{tabular}{rcl}
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ 
-  @{text "ABS (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
-  @{text "REP (\<sigma>, \<sigma>)"} & $\dn$ & @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{function types:}\\ 
-  @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
-  @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} & $\dn$ & @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ 
-  @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
-  @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s
-  \<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\\
-  @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
-  @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
+  \begin{tabular}{@ {\hspace{2mm}}l@ {}}
+  \multicolumn{1}{@ {}l}{equal types:}\\ 
+  @{text "ABS (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\\
+  @{text "REP (\<sigma>, \<sigma>)"} $\dn$ @{text "id :: \<sigma> \<Rightarrow> \<sigma>"}\smallskip\\
+  \multicolumn{1}{@ {}l}{function types:}\\ 
+  @{text "ABS (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} $\dn$ @{text "REP (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> ABS (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\\
+  @{text "REP (\<sigma>\<^isub>1 \<Rightarrow> \<sigma>\<^isub>2, \<tau>\<^isub>1 \<Rightarrow> \<tau>\<^isub>2)"} $\dn$ @{text "ABS (\<sigma>\<^isub>1, \<tau>\<^isub>1) \<singlearr> REP (\<sigma>\<^isub>2, \<tau>\<^isub>2)"}\smallskip\\
+  \multicolumn{1}{@ {}l}{equal type constructors:}\\ 
+  @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "map_\<kappa> (ABS (\<sigma>s, \<tau>s))"}\\
+  @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "map_\<kappa> (REP (\<sigma>s, \<tau>s))"}\smallskip\\
+  \multicolumn{1}{@ {}l}{unequal type constructors:}\\
+  @{text "ABS (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "Abs_\<kappa>\<^isub>q \<circ> (MAP(\<rho>s \<kappa>) (ABS (\<sigma>s', \<tau>s)))"}\\
+  @{text "REP (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "(MAP(\<rho>s \<kappa>) (REP (\<sigma>s', \<tau>s))) \<circ> Rep_\<kappa>\<^isub>q"}
   \end{tabular}\hfill\numbered{ABSREP}
   \end{center}
   %
@@ -597,7 +602,7 @@
   type as follows:
   %
   \begin{center}
-  \begin{tabular}{rcl}
+  \begin{tabular}{r@ {\hspace{1mm}}c@ {\hspace{1mm}}l}
   @{text "MAP' (\<alpha>)"} & $\dn$ & @{text "a\<^sup>\<alpha>"}\\
   @{text "MAP' (\<kappa>)"} & $\dn$ & @{text "id :: \<kappa> \<Rightarrow> \<kappa>"}\\
   @{text "MAP' (\<sigma>s \<kappa>)"} & $\dn$ & @{text "map_\<kappa> (MAP'(\<sigma>s))"}\smallskip\\
@@ -640,7 +645,10 @@
   the abstraction function
 
   \begin{isabelle}\ \ \ \ \ %%%
-  @{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr> Abs_fset \<circ> map_list id"}
+  \begin{tabular}{l}
+  @{text "(map_list (map_list id \<circ> Rep_fset) \<circ> Rep_fset) \<singlearr>"}\\
+  \mbox{}\hspace{4.5cm}@{text " Abs_fset \<circ> map_list id"}
+  \end{tabular}
   \end{isabelle}
 
   \noindent
@@ -705,7 +713,7 @@
   \end{proof}
 *}
 
-section {* Respectfulness and Preservation \label{sec:resp} *}
+section {* Respectfulness and\\ Preservation \label{sec:resp} *}
 
 text {*
   The main point of the quotient package is to automatically ``lift'' theorems
@@ -717,10 +725,12 @@
   notable is the bound variable function, that is the constant @{text bn}, defined 
   for raw lambda-terms as follows
 
-  \begin{isabelle}\ \ \ \ \ %%%
+  \begin{isabelle}
+  \begin{center}
   @{text "bn (x) \<equiv> \<emptyset>"}\hspace{4mm}
-  @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\hspace{4mm}
+  @{text "bn (t\<^isub>1 t\<^isub>2) \<equiv> bn (t\<^isub>1) \<union> bn (t\<^isub>2)"}\smallskip\\
   @{text "bn (\<lambda>x. t) \<equiv> {x} \<union> bn (t)"}
+  \end{center}
   \end{isabelle}
 
   \noindent
@@ -744,20 +754,19 @@
 
   \begin{center}
   \hfill
-  \begin{tabular}{rcl}
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{equal types:}\\ 
-  @{text "REL (\<sigma>, \<sigma>)"} & $\dn$ & @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
-   \multicolumn{3}{@ {\hspace{-4mm}}l}{equal type constructors:}\\ 
-  @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} & $\dn$ & @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{unequal type constructors with @{text "\<alpha>s
-  \<kappa>\<^isub>q"} being the quotient of the raw type @{text "\<rho>s \<kappa>"}:}\smallskip\\
-  @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} & $\dn$ & @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
+  \begin{tabular}{l}
+  \multicolumn{1}{@ {}l}{equal types:}\\ 
+  @{text "REL (\<sigma>, \<sigma>)"} $\dn$ @{text "= :: \<sigma> \<Rightarrow> \<sigma> \<Rightarrow> bool"}\smallskip\\
+   \multicolumn{1}{@ {}l}{equal type constructors:}\\ 
+  @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>)"} $\dn$ @{text "rel_\<kappa> (REL (\<sigma>s, \<tau>s))"}\smallskip\\
+  \multicolumn{1}{@ {}l}{unequal type constructors:}\\
+  @{text "REL (\<sigma>s \<kappa>, \<tau>s \<kappa>\<^isub>q)"} $\dn$ @{text "rel_\<kappa>\<^isub>q (REL (\<sigma>s', \<tau>s))"}\\
   \end{tabular}\hfill\numbered{REL}
   \end{center}
 
   \noindent
   The @{text "\<sigma>s'"} in the last clause are calculated as in \eqref{ABSREP}:
-  we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type 
+  again we know that type @{text "\<alpha>s \<kappa>\<^isub>q"} is the quotient of the raw type 
   @{text "\<rho>s \<kappa>"}. The @{text "\<sigma>s'"} are the substitutions for @{text "\<alpha>s"} obtained by matching 
   @{text "\<rho>s \<kappa>"} and @{text "\<sigma>s \<kappa>"}.
 
@@ -957,27 +966,27 @@
   the structure of  @{text "raw_thm"} and @{text "quot_thm"} as follows:
 
   \begin{center}
-  \begin{tabular}{rcl}
-  \multicolumn{3}{@ {}l}{abstractions:}\smallskip\\
-  @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} & $\dn$ & 
+  \begin{tabular}{l}
+  \multicolumn{1}{@ {}l}{abstractions:}\smallskip\\
+  @{text "REG (\<lambda>x\<^sup>\<sigma>. t, \<lambda>x\<^sup>\<tau>. s)"} $\dn$ 
   $\begin{cases}
   @{text "\<lambda>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
   @{text "\<lambda>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
   \end{cases}$\smallskip\\
   \\
-  \multicolumn{3}{@ {}l}{universal quantifiers:}\\
-  @{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} & $\dn$ & 
+  \multicolumn{1}{@ {}l}{universal quantifiers:}\\
+  @{text "REG (\<forall>x\<^sup>\<sigma>. t, \<forall>x\<^sup>\<tau>. s)"} $\dn$
   $\begin{cases}
   @{text "\<forall>x\<^sup>\<sigma>. REG (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
   @{text "\<forall>x\<^sup>\<sigma> \<in> Respects (REL (\<sigma>, \<tau>)). REG (t, s)"}
   \end{cases}$\smallskip\\
-  \multicolumn{3}{@ {}l}{equality:}\smallskip\\
+  \multicolumn{1}{@ {}l}{equality:}\smallskip\\
   %% REL of two equal types is the equality so we do not need a separate case
-  @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} & $\dn$ & @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\
-  \multicolumn{3}{@ {}l}{applications, variables and constants:}\\
-  @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} & $\dn$ & @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
-  @{text "REG (x\<^isub>1, x\<^isub>2)"} & $\dn$ & @{text "x\<^isub>1"}\\
-  @{text "REG (c\<^isub>1, c\<^isub>2)"} & $\dn$ & @{text "c\<^isub>1"}\\
+  @{text "REG (=\<^bsup>\<sigma>\<Rightarrow>\<sigma>\<Rightarrow>bool\<^esup>, =\<^bsup>\<tau>\<Rightarrow>\<tau>\<Rightarrow>bool\<^esup>)"} $\dn$ @{text "REL (\<sigma>, \<tau>)"}\\\smallskip\\
+  \multicolumn{1}{@ {}l}{applications, variables and constants:}\\
+  @{text "REG (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2)"} $\dn$ @{text "REG (t\<^isub>1, s\<^isub>1) REG (t\<^isub>2, s\<^isub>2)"}\\
+  @{text "REG (x\<^isub>1, x\<^isub>2)"} $\dn$ @{text "x\<^isub>1"}\\
+  @{text "REG (c\<^isub>1, c\<^isub>2)"} $\dn$ @{text "c\<^isub>1"}\\
   \end{tabular}
   \end{center}
   %
@@ -991,26 +1000,26 @@
   terms) and returns @{text "inj_thm"}:
 
   \begin{center}
-  \begin{tabular}{rcl}
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{abstractions:}\\
-  @{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ & 
-  $\begin{cases}
+  \begin{tabular}{l}
+  \multicolumn{1}{@ {}l}{abstractions:}\\
+  @{text "INJ (\<lambda>x. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} $\dn$\\ 
+  \hspace{18mm}$\begin{cases}
   @{text "\<lambda>x. INJ (t, s)"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
   @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x. INJ (t, s)))"}
-  \end{cases}$\\
-  @{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} & $\dn$ 
-  & @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{universal quantifiers:}\\
-  @{text "INJ (\<forall> t, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s)"}\\
-  @{text "INJ (\<forall> t \<in> R, \<forall> s) "} & $\dn$ & @{text "\<forall> INJ (t, s) \<in> R"}\smallskip\\
-  \multicolumn{3}{@ {\hspace{-4mm}}l}{applications, variables and constants:}\smallskip\\
-  @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} & $\dn$ & @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
-  @{text "INJ (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} & $\dn$ & 
+  \end{cases}$\smallskip\\
+  @{text "INJ (\<lambda>x \<in> R. t :: \<sigma>, \<lambda>x. s :: \<tau>) "} $\dn$\\ 
+  \hspace{18mm}@{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) (\<lambda>x \<in> R. INJ (t, s)))"}\smallskip\\
+  \multicolumn{1}{@ {}l}{universal quantifiers:}\\
+  @{text "INJ (\<forall> t, \<forall> s) "} $\dn$ @{text "\<forall> INJ (t, s)"}\\
+  @{text "INJ (\<forall> t \<in> R, \<forall> s) "} $\dn$ @{text "\<forall> INJ (t, s) \<in> R"}\smallskip\\
+  \multicolumn{1}{@ {}l}{applications, variables and constants:}\smallskip\\
+  @{text "INJ (t\<^isub>1 t\<^isub>2, s\<^isub>1 s\<^isub>2) "} $\dn$ @{text " INJ (t\<^isub>1, s\<^isub>1) INJ (t\<^isub>2, s\<^isub>2)"}\\
+  @{text "INJ (x\<^isub>1\<^sup>\<sigma>, x\<^isub>2\<^sup>\<tau>) "} $\dn$
   $\begin{cases}
   @{text "x\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
   @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) x\<^isub>1)"}\\
   \end{cases}$\\
-  @{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} & $\dn$ & 
+  @{text "INJ (c\<^isub>1\<^sup>\<sigma>, c\<^isub>2\<^sup>\<tau>) "} $\dn$ 
   $\begin{cases}
   @{text "c\<^isub>1"} \quad\mbox{provided @{text "\<sigma> = \<tau>"}}\\
   @{text "REP (\<sigma>, \<tau>) (ABS (\<sigma>, \<tau>) c\<^isub>1)"}\\