Index: /reasoner/consTranslation.tex
===================================================================
--- /reasoner/consTranslation.tex	(revision 151)
+++ /reasoner/consTranslation.tex	(revision 152)
@@ -245,7 +245,7 @@
 \subsection{Container types}\label{sectContainerDefaults}
 
-Per se, a container variable can only declare the contained type and the respective element values through its default, i.e., there is no direct opportunity to define constraints for a container. However, constraints are indirectly defined through the contained type and the types used for the individual elements. Here, compounds, derived types, constraint types and, transitively, nested containers can introduce constraints further characterizing (the contents of) a container variable. Reference types do not need specific treatment as constraints are translated for the target variable of the reference. Basic types cannot define own containers. Due to refinement, all relevant types may be more specific than the (generic) container type given for the initial container variable. 
-
-Containers differ from the other IVML types as a container may contain an arbitrary number of elements. Thus, for specifying a constraint over a container, we must apply all-quantification or, as an alternative, unroll the container, create constraints for the individual container entries and take care of the changes of the elements. Currently, unrolling is not possible for all IVML container types, e.g., set-based types do not offer index-based access. Thus, for the translation pattern, we generically use quantification.
+As a generic type, an IVML container variable can only declare the contained element type. Moreover, a container differs from other IVML types, as a container can hold an arbitrary number of elements. The element values can be defined through a default value expression or an assignment constraint. Thus, there is no direct opportunity to define constraints for a container. However, constraints can be imposed indirectly if a container acts as base type for a derived type, through the contained type or the actual type of the individual element. If the element type is a compound, a derived type, a constraint type or, transitively, a nested container, the specific type indirectly imposes constraints further characterizing (the contents of) a container variable. The actual element type is important, in particular for elements of a container type, as due to type refinements an individual container element may have a more specific type than the element type defined by the container type. For the element type, a reference type appears to be transparent, i.e., constraints are imposed by the target type of the reference and basic types do not impose further constraints as no own constraints can be defined on them. 
+
+As containers can hold an arbitrary number of elements, specifying a constraint over a container typically involves quantification, usually all-quantification. As an alternative, we might internally unroll a container for reasoning, create constraints for the individual elements and take care of the changes of the individual element variables. Although potentially more efficient in some cases, unrolling is not possible for all IVML container types, e.g., set-based types do not offer an index-based access to the elements. Thus, as a generic uniform translation pattern, we apply quantification.
 
 \grayPara{
