diff --git a/frontend/styles/view/type-inference.css b/frontend/styles/view/type-inference.css
index 4d1d7e5..672e07f 100644
--- a/frontend/styles/view/type-inference.css
+++ b/frontend/styles/view/type-inference.css
@@ -41,7 +41,9 @@
 }
 
 tc-explanation {
-	width: 100em;
+	width: 25em;
+	flex-shrink: 0;
+	flex-grow: 0;
 	padding-left: 1em;
 	padding-right: 1em;
 	overflow-y: auto;
diff --git a/src/main/resources/language/translation_en.properties b/src/main/resources/language/translation_en.properties
index bad6388..c0f6785 100644
--- a/src/main/resources/language/translation_en.properties
+++ b/src/main/resources/language/translation_en.properties
@@ -218,9 +218,9 @@ expUnification.mgu=In this step the most general unifier %0% for the set of cons
 expUnification.finalType=In this step the most general unifier %0% is applied to the type %1% of the input. The result %2% \
  is the final type of the input.
 expUnification.infiniteType=The same type variable appears on both sides of the constraint. Since this would cause an \
- infinite type, the execution of the unification is stopped.
-expUnification.differentTypes=Since the types on both sides of the constraint are incompatible, the execution of the \
- unification is stopped.
+ infinite type, the unification algorithm terminates.
+expUnification.differentTypes=Since the types on both sides of the constraint are incompatible, the \
+unification algorithm terminates.
 expLetUnification.finalType=In this step the most general unifier %0% is applied to the type %1% of the let-definition. \
  The result %2% is the final type of the let-definition.
 expLetUnification.typeAss=In this step the type assumptions %0% for the further execution of the algorithm are \