diff --git a/src/main/scala/hb/dhbw/FJTypeinference.scala b/src/main/scala/hb/dhbw/FJTypeinference.scala
index 9b97ceb..5a386af 100644
--- a/src/main/scala/hb/dhbw/FJTypeinference.scala
+++ b/src/main/scala/hb/dhbw/FJTypeinference.scala
@@ -78,6 +78,11 @@ object FJTypeinference {
     Class(in.name, in.genericParams, in.superType, in.fields, newMethods.toList)
   }
 
+  def sigmaReplace(sigma:Map[String, Type], unifyType: UnifyType): Type = unifyType match {
+    case UnifyRefType(n, ps) => RefType(n, ps.map(it => sigmaReplace(sigma, it)))
+    case UnifyTV(a) => sigma(a)
+  }
+
   def typeinference(str: String): Either[String, (Set[Set[UnifyConstraint]], List[Class])] = {
     val ast = Parser.parse(str).map(ASTBuilder.fromParseTree(_))
     var typedClasses: List[Class] = List()
@@ -87,8 +92,26 @@ object FJTypeinference {
         val newClassList = cOld :+ c
         val typeResult = TYPE.generateConstraints(newClassList, generateFC(newClassList))
         val unifyResult = Unify.unifyIterative(convertOrConstraints(typeResult._1), typeResult._2)
+        // Unify step 6:
+        val genericNames = c.genericParams.map(_._1).map(_ match{case GenericType(x) => x})
+        val sigma = unifyResult.map(result => {
+          val lessdotSigma = result.filter(_ match {
+            case UnifyLessDot(UnifyTV(a), _) => true
+            case _ => false
+          }).map(_ match{
+            case UnifyLessDot(UnifyTV(a), UnifyRefType(n, _)) =>
+              if (genericNames.find(_ == n).isDefined) (a -> GenericType(n)) else (a -> GenericType(a))
+          }).toMap[String, Type]
+          val eqDotSigma = result.map(_ match{
+            case UnifyEqualsDot(UnifyTV(a), toRefType) => (a -> sigmaReplace(lessdotSigma, toRefType))
+            case UnifyLessDot(UnifyTV(a), UnifyRefType(n, p)) => (a -> GenericType(a))
+          }).toMap
+          //merge the two maps:
+          lessdotSigma ++ eqDotSigma
+        }).toList.head
+        val generics:Set[(Type, Type)] = Set()
         //Insert intersection types
-        val typeInsertedC = InsertTypes.insert(unifyResult, c)
+        val typeInsertedC = InsertTypes.applyResult(sigma, generics, c)//InsertTypes.insert(unifyResult, c)
         typedClasses = typedClasses :+ typeInsertedC
         unifyResults = unifyResults + unifyResult
         cOld :+ typeInsertedC
diff --git a/src/main/scala/hb/dhbw/InsertTypes.scala b/src/main/scala/hb/dhbw/InsertTypes.scala
index a0d6677..f781967 100644
--- a/src/main/scala/hb/dhbw/InsertTypes.scala
+++ b/src/main/scala/hb/dhbw/InsertTypes.scala
@@ -32,6 +32,9 @@ object InsertTypes {
     ret ++ alessdotB.map(cons => UnifyEqualsDot(cons.left, cons.right))
   }
 
+  def applyResult(sigma: Map[String, Type], generics: Set[(Type, Type)], into: Class): Class = {
+    //TODO
+  }
 
   def insert(unifyResult: Set[Set[UnifyConstraint]], into: Class): Class = {
 
diff --git a/src/main/scala/hb/dhbw/TYPE.scala b/src/main/scala/hb/dhbw/TYPE.scala
index b1be638..9a3422c 100644
--- a/src/main/scala/hb/dhbw/TYPE.scala
+++ b/src/main/scala/hb/dhbw/TYPE.scala
@@ -73,8 +73,9 @@ object TYPE {
         val es = params.map(ex => TYPEExpr(ex, localVars, ast))
         val methods = findMethods(name, es.size, ast)
         val consM = methods.map(m => AndConstraint(m._2.genericParams ++
-          List(EqualsDot(rty, cToType(m._1)), EqualsDot(a, m._2.retType))
+          List(LessDot(rty, cToType(m._1)), EqualsDot(a, m._2.retType))
           ++ m._2.params.map(_._1).zip(es.map(_._1)).map(a => LessDot(a._2, a._1))
+          ++ m._1.genericParams.map(it => LessDot(it._1, it._2))
         ))
         val retCons = (cons ++ es.flatMap(_._2) ++ List(OrConstraint(consM)))
         (a, genericReplace.replaceGenerics(retCons))
diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala
index b19637e..5a6c278 100644
--- a/src/main/scala/hb/dhbw/Unify.scala
+++ b/src/main/scala/hb/dhbw/Unify.scala
@@ -35,6 +35,20 @@ object Unify {
     override def result: Set[UnifyConstraint] = eq
   }
 
+  def removeALessdotB(eq: Set[UnifyConstraint]): Set[UnifyConstraint] = {
+    var ret = eq
+    val alessdotb = eq.filter(_ match{
+      case UnifyLessDot(UnifyTV(a), UnifyTV(b)) => true
+      case _ => false
+    })
+    alessdotb.foreach(it => ret = subst(it.left.asInstanceOf[UnifyTV], it.right, ret))
+    ret.filter(_ match{
+      case UnifyEqualsDot(UnifyTV(a), UnifyTV(b)) => a != b
+      case UnifyLessDot(UnifyTV(_), UnifyTV(_)) => false
+      case _ => true
+    }) ++ alessdotb.map(_ match {case UnifyLessDot(a, b) => UnifyEqualsDot(a,b)})
+  }
+
   def unifyIterative(orCons: Set[Set[Set[UnifyConstraint]]], fc: FiniteClosure) : Set[Set[UnifyConstraint]] = {
     def getNext[A](from: Set[CartesianProduct[A]])=
       from.find(_.hasNext()).map(it => it.nextProduct())
@@ -51,7 +65,7 @@ object Unify {
         val substResult = substStep(step2Result.nextProduct().flatten)
         substResult match{
           case UnchangedSet(eq) => if(isSolvedForm(eq)){
-            results = results + eq
+            results = results + removeALessdotB(eq)
           }
           case ChangedSet(eq) =>
             eqSets = eqSets + new CartesianProduct[Set[UnifyConstraint]](Set(Set(eq)))