diff --git a/src/main/scala/hb/dhbw/FJTypeinference.scala b/src/main/scala/hb/dhbw/FJTypeinference.scala
index d8fc68a..5e62062 100644
--- a/src/main/scala/hb/dhbw/FJTypeinference.scala
+++ b/src/main/scala/hb/dhbw/FJTypeinference.scala
@@ -75,6 +75,17 @@ object FJTypeinference {
     Class(in.name, in.genericParams, in.superType, in.fields, newMethods.toList)
   }
 
+  def removeLessDotGenericConstraints(unifyResult: Set[Set[UnifyConstraint]], generics: Set[String]) :Set[Set[UnifyConstraint]] =
+    unifyResult.map(_.map( _ match { //
+      case UnifyLessDot(UnifyTV(a), UnifyRefType(name, List())) =>
+        if(generics.contains(name))
+            UnifyEqualsDot(UnifyTV(a), UnifyRefType(name, List()))
+          else
+            UnifyLessDot(UnifyTV(a), UnifyRefType(name, List()))
+      case x => x
+    }
+  ))
+
   def typeinference(str: String): Either[String, List[Class]] = {
     val ast = Parser.parse(str).map(ASTBuilder.fromParseTree(_))
     var typedClasses: List[Class] = List()
@@ -85,9 +96,10 @@ object FJTypeinference {
         val typeResult = TYPE.generateConstraints(newClassList, fc)
         val unifyResult = Unify.unifyIterative(convertOrConstraints(typeResult._1), typeResult._2)
 
+        val postProcessed = removeLessDotGenericConstraints(unifyResult, c.genericParams.map(_._1.asInstanceOf[GenericType].name).toSet)
         //Insert intersection types
         //val typeInsertedC = InsertTypes.applyResult(sigma, generics, c)//InsertTypes.insert(unifyResult, c)
-        val typeInsertedC = removeOverloadedSubtypeMethods(InsertTypes.applyUnifyResult(unifyResult, c), fc)
+        val typeInsertedC = removeOverloadedSubtypeMethods(InsertTypes.applyUnifyResult(postProcessed, c), fc)
         typedClasses = typedClasses :+ typeInsertedC
         cOld :+ typeInsertedC
       })
diff --git a/src/main/scala/hb/dhbw/InsertTypes.scala b/src/main/scala/hb/dhbw/InsertTypes.scala
index 667b58c..94ec681 100644
--- a/src/main/scala/hb/dhbw/InsertTypes.scala
+++ b/src/main/scala/hb/dhbw/InsertTypes.scala
@@ -5,7 +5,7 @@ object InsertTypes {
 
   // Unify step 6:
   //TODO: a <. X must be replaced by X -> sigma(a) = GenericType(X) in that case
-  private class UnifyResult(solvedCons: Set[UnifyConstraint]){
+  private class UnifyResult(solvedCons: Set[UnifyConstraint], genericNames: Set[String]){
     def sigma(x: Type): Type = x match {
       case TypeVariable(n) => sigma(UnifyTV(x.asInstanceOf[TypeVariable].name))
       case v => v
@@ -14,11 +14,13 @@ object InsertTypes {
         case UnifyTV(n) => {
           val to = solvedCons.find(_.left == x).get
           to match {
-            case UnifyEqualsDot(UnifyTV(_), UnifyTV(x)) => this.sigma(UnifyTV(x))
+            case UnifyEqualsDot(UnifyTV(_), UnifyTV(x)) => GenericType(x)
+            case UnifyEqualsDot(UnifyTV(_), UnifyRefType(n, List())) => if(genericNames.contains(n)) GenericType(n) else RefType(n, List())
             case UnifyEqualsDot(UnifyTV(_), UnifyRefType(n, ps)) => RefType(n, ps.map(this.sigma(_)))
             case UnifyLessDot(UnifyTV(x), UnifyRefType(n, ps)) => GenericType(x)
           }
         }
+        case UnifyRefType(n, List()) => if(genericNames.contains(n)) GenericType(n) else RefType(n, List())
         case UnifyRefType(n, ps) => RefType(n, ps.map(sigma))
       }
 
@@ -34,7 +36,7 @@ object InsertTypes {
   def applyUnifyResult(eq: Set[Set[UnifyConstraint]], into: Class) = {
     val newMethods = into.methods.flatMap(m => {
       eq.map(req => {
-        val result = new UnifyResult(req)
+        val result = new UnifyResult(req, into.genericParams.map(_._1.asInstanceOf[GenericType].name).toSet)
         Method(result.delta(), result.sigma(m.retType), m.name, m.params.map(p => (result.sigma(p._1), p._2)), m.retExpr)
       })
     })
diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala
index ab3387d..006071b 100644
--- a/src/main/scala/hb/dhbw/Unify.scala
+++ b/src/main/scala/hb/dhbw/Unify.scala
@@ -24,19 +24,24 @@ object Unify {
     override def result: Set[UnifyConstraint] = eq
   }
 
-  def removeALessdotB(eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
+  def postProcessing(eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
     var ret = eq
-    val alessdotb:Set[UnifyConstraint] = eq.filter(_ match{
+    var ruleResult = subElimRule(ret)
+    while(ruleResult.isDefined){
+      ret = ruleResult.get
+      ruleResult = subElimRule(ruleResult.get)
+    }
+    ret
+  }
+
+  def subElimRule(eq: Set[UnifyConstraint]) : Option[Set[UnifyConstraint]] = {
+    var ret = eq
+    eq.find(_ match{
       case UnifyLessDot(UnifyTV(a), UnifyTV(b)) => true
       case _ => false
+    }).map(it => {
+      subst(it.right.asInstanceOf[UnifyTV], it.left, ret.filter(it != _)) ++ Set(UnifyEqualsDot(it.right, it.left), UnifyEqualsDot(it.left, it.left))
     })
-    ret = ret.filter(it => !alessdotb.contains(it))
-    var newADotEqB : Set[UnifyConstraint] = Set()
-    alessdotb.foreach(it => {
-      ret = subst(it.left.asInstanceOf[UnifyTV], it.right, ret)
-      newADotEqB = newADotEqB ++ Set(UnifyEqualsDot(it.right, it.left))
-    })
-    ret ++ alessdotb.map(_ match {case UnifyLessDot(a, b) => UnifyEqualsDot(a,b)}) ++ newADotEqB
   }
 
   def unifyIterative(orCons: Set[Set[Set[UnifyConstraint]]], fc: FiniteClosure) : Set[Set[UnifyConstraint]] = {
@@ -55,7 +60,7 @@ object Unify {
         val substResult = substStep(step2Result.nextProduct().flatten)
         substResult match{
           case UnchangedSet(eq) => if(isSolvedForm(eq)){
-            results = results + removeALessdotB(eq)
+            results = results + postProcessing(eq)
           }
           case ChangedSet(eq) =>
             eqSets = eqSets + new CartesianProduct[Set[UnifyConstraint]](Set(Set(eq)))
diff --git a/src/test/scala/IntegrationTest.scala b/src/test/scala/IntegrationTest.scala
index b844f16..3ecfb2e 100644
--- a/src/test/scala/IntegrationTest.scala
+++ b/src/test/scala/IntegrationTest.scala
@@ -108,6 +108,12 @@ class IntegrationTest extends FunSuite {
     val result = FJTypeinference.typeinference(input)
     println(result.map(it => Main.prettyPrintAST(it)))
   }
+
+  test("ListExample") {
+    val input = "\n\nclass List<A extends Object> extends Object{\n    A element;\n    List<A> succ; \n    add(a){\n       return new List(a, this);\n    }\n\n}\n\nclass Example extends Object{\n\n    test(a){\n        return a.add(this);\n    }\n}"
+    val result = FJTypeinference.typeinference(input)
+    println(result.map(it => Main.prettyPrintAST(it)))
+  }
   /*
 
 class List<A extends Object> extends Object{
diff --git a/src/test/scala/UnifyTest.scala b/src/test/scala/UnifyTest.scala
index 0090605..9351937 100644
--- a/src/test/scala/UnifyTest.scala
+++ b/src/test/scala/UnifyTest.scala
@@ -1,5 +1,6 @@
 
-import hb.dhbw.{FiniteClosure, RefType, TypeVariable, Unify, UnifyConstraint, UnifyEqualsDot, UnifyLessDot, UnifyRefType, UnifyTV}
+
+import hb.dhbw.{FJNamedType, FiniteClosure, RefType, TypeVariable, Unify, UnifyConstraint, UnifyEqualsDot, UnifyLessDot, UnifyRefType, UnifyTV}
 import org.scalatest.FunSuite
 
 class UnifyTest extends FunSuite {
@@ -11,12 +12,19 @@ class UnifyTest extends FunSuite {
 
   test("sub-elim rule"){
     val input : Set[UnifyConstraint] = Set(UnifyLessDot(UnifyTV("a"), UnifyTV("b")), UnifyEqualsDot(UnifyTV("a"), UnifyRefType("a", List())))
-    val result = Unify.removeALessdotB(input)
+    val result = Unify.postProcessing(input)
     println(result)
     assert(result.contains(UnifyEqualsDot(UnifyTV("a"), UnifyTV("b"))))
     assert(result.contains(UnifyEqualsDot(UnifyTV("b"), UnifyTV("a"))))
   }
 
+  test("error"){
+    val input : Set[Set[Set[UnifyConstraint]]]= Set(Set(Set(UnifyLessDot(UnifyTV("1"), UnifyTV("B")), UnifyLessDot(UnifyTV("1"), UnifyTV("2")),
+      UnifyLessDot(UnifyRefType("Test", List()), UnifyTV("2")))))
+    val result = Unify.unifyIterative(input, new FiniteClosure(Set((FJNamedType("Test", List()), FJNamedType("Object", List())))))
+    println(result)
+  }
+
   /*
   test("Unify.step2") {
     var step2 = Unify.step2(Set(UnifyLessDot(TypeVariable("a"), TypeVariable("b")),