--- a/Quotient-Paper/Paper.thy	Sat Jun 05 10:03:42 2010 +0200
+++ b/Quotient-Paper/Paper.thy	Sat Jun 05 14:37:05 2010 +0200
@@ -501,19 +501,30 @@
 subsection {* Injection *}
 
 text {*
+  The injection proof starts with an equality between the regularized theorem
+  and the injected version. The proof again follows by the structure of the
+  two term, and is defined for a goal being a relation between the two terms.
 
-  The 2 key lemmas are:
+  \begin{itemize}
+  \item For two constants, an appropriate constant respectfullness assumption is used.
+  \item For two variables, the regularization assumptions state that they are related.
+  \item For two abstractions, they are eta-expanded and beta-reduced.
+  \end{itemize}
 
-  @{thm [display] apply_rsp[no_vars]}
+  Otherwise the two terms are applications. There are two cases: If there is a REP/ABS
+  in the injected theorem we can use the theorem:
+
   @{thm [display] rep_abs_rsp[no_vars]}
 
+  and continue the proof.
 
+  Otherwise we introduce an appropriate relation between the subterms and continue with
+  two subgoals using the lemma:
+
+  @{thm [display] apply_rsp[no_vars]}
 
 *}
 
-
-
-
 subsection {* Cleaning *}
 
 text {* Preservation of quantifiers, abstractions, relations, quotient-constants