diff --git a/index.html b/index.html
index d0b0c96..7c098bd 100644
--- a/index.html
+++ b/index.html
@@ -18,11 +18,8 @@
           <pre><div id="ast-output"></div></pre>
       </div>
   </div>
-  <div id="bottom">
-      <div id="unify-output"></div>
-  </div>
   <script type="text/javascript" src="highlight.min.js"></script>
-  <script type="text/javascript" src="target/scala-2.13/fj-typeinference-fastopt/main.js"></script>
+  <script type="text/javascript" src="target/scala-2.13/fj-typeinference-opt/main.js"></script>
   <br/>
   <p>Credit: the layout of this page was shamelessly stolen from <a href="https://github.com/LPTK/simple-algebraic-subtyping">the Simple-sub demo page</a>.</p>
   </body>
diff --git a/src/main/scala/hb/dhbw/FJTypeinference.scala b/src/main/scala/hb/dhbw/FJTypeinference.scala
index 5a386af..ee6d80f 100644
--- a/src/main/scala/hb/dhbw/FJTypeinference.scala
+++ b/src/main/scala/hb/dhbw/FJTypeinference.scala
@@ -83,46 +83,21 @@ object FJTypeinference {
     case UnifyTV(a) => sigma(a)
   }
 
-  def typeinference(str: String): Either[String, (Set[Set[UnifyConstraint]], List[Class])] = {
+  def typeinference(str: String): Either[String, List[Class]] = {
     val ast = Parser.parse(str).map(ASTBuilder.fromParseTree(_))
     var typedClasses: List[Class] = List()
-    val typeResult = ast.map(ast => {
-      var unifyResults = Set[Set[Set[UnifyConstraint]]]()
+    ast.map(ast => {
       ast.foldLeft(List[Class]())((cOld, c) => {
         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.applyResult(sigma, generics, c)//InsertTypes.insert(unifyResult, c)
+        //val typeInsertedC = InsertTypes.applyResult(sigma, generics, c)//InsertTypes.insert(unifyResult, c)
+        val typeInsertedC = InsertTypes.applyUnifyResult(unifyResult, c)
         typedClasses = typedClasses :+ typeInsertedC
-        unifyResults = unifyResults + unifyResult
         cOld :+ typeInsertedC
       })
-      unifyResults
     })
-    val fc = generateFC(typedClasses)
-    typedClasses =
-    typedClasses.map(cl => {
-      removeOverloadedSubtypeMethods(cl, fc)
-    })
-    typeResult.map(it => (it.flatten, typedClasses))
   }
 }
diff --git a/src/main/scala/hb/dhbw/InsertTypes.scala b/src/main/scala/hb/dhbw/InsertTypes.scala
index 1c83692..451b779 100644
--- a/src/main/scala/hb/dhbw/InsertTypes.scala
+++ b/src/main/scala/hb/dhbw/InsertTypes.scala
@@ -2,6 +2,45 @@ package hb.dhbw
 
 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]){
+    def sigma(x: Type): Type = x match {
+      case TypeVariable(n) => sigma(UnifyTV(x.asInstanceOf[TypeVariable].name))
+      case v => v
+    }
+    def sigma(x: UnifyType): Type = { x match {
+        case UnifyTV(n) => {
+          val to = solvedCons.find(_.left == x).get
+          to match {
+            case UnifyEqualsDot(UnifyTV(_), UnifyTV(x)) => this.sigma(UnifyTV(x))
+            case UnifyEqualsDot(UnifyTV(_), UnifyRefType(n, ps)) => RefType(n, ps.map(this.sigma(_)))
+            case UnifyLessDot(UnifyTV(x), UnifyRefType(n, ps)) => GenericType(x)
+          }
+        }
+        case UnifyRefType(n, ps) => RefType(n, ps.map(sigma))
+      }
+
+    }
+
+    def delta() = {
+      solvedCons.collect{
+        case UnifyLessDot(UnifyTV(a), UnifyRefType(n, ps)) => LessDot(GenericType(a), RefType(n, ps.map(sigma)))
+      }.toList
+    }
+  }
+
+  def applyUnifyResult(eq: Set[Set[UnifyConstraint]], into: Class) = {
+    val newMethods = into.methods.flatMap(m => {
+      eq.map(req => {
+        val result = new UnifyResult(req)
+        Method(result.delta(), result.sigma(m.retType), m.name, m.params.map(p => (result.sigma(p._1), p._2)), m.retExpr)
+      })
+    })
+    Class(into.name, into.genericParams, into.superType, into.fields, newMethods)
+  }
+
   /**
    * Remove a <. b constraints
    * @param eq
diff --git a/src/main/scala/hb/dhbw/Main.scala b/src/main/scala/hb/dhbw/Main.scala
index dfc6497..ede4633 100644
--- a/src/main/scala/hb/dhbw/Main.scala
+++ b/src/main/scala/hb/dhbw/Main.scala
@@ -20,10 +20,9 @@ class HLJSResult extends js.Object{
 }
 
 object Main {
-
   def main(args: Array[String]): Unit = {
     val source = document.querySelector("#fj-input")
-    update(source.textContent)
+    //update(source.textContent)
     source.addEventListener("input", typecheck)
   }
   @JSExportTopLevel("typecheck")
@@ -35,19 +34,14 @@ object Main {
   }
 
   def update(str: String): Unit = {
-    val target = document.querySelector("#unify-output")
     val tiResult = FJTypeinference.typeinference(str)
-    target.innerHTML = tiResult.fold(
-      (error) => error,
-      (result) => prettyPrintHTML(result._1)
-    )
     val astOutput = document.querySelector("#ast-output")
     astOutput.innerHTML = tiResult.fold(
       (error) => Parser.parse(str).map( parseTree =>
         hljs.highlightAuto(prettyPrintAST(ASTBuilder.fromParseTree(parseTree))).value
       ).merge,
       (result) => {
-          hljs.highlightAuto(prettyPrintAST(result._2)).value
+          hljs.highlightAuto(prettyPrintAST(result)).value
       }
     )
 
diff --git a/src/main/scala/hb/dhbw/Unify.scala b/src/main/scala/hb/dhbw/Unify.scala
index 6b08927..9eea652 100644
--- a/src/main/scala/hb/dhbw/Unify.scala
+++ b/src/main/scala/hb/dhbw/Unify.scala
@@ -20,18 +20,6 @@ final case class AEqualsB(a: TypeVariable, b: TypeVariable) extends UnifyResultC
 final case class AEqualsN(a: TypeVariable, n: ResultRefType) extends UnifyResultConstraint
 */
 
-class UnifyResult(solvedCons: Set[UnifyConstraint]){
-  def sigma(x: UnifyType): UnifyType = {
-    assert(x.isInstanceOf[UnifyTV])
-    val to = solvedCons.find(_.left == x).get
-    to match {
-      case UnifyEqualsDot(_, UnifyTV(x)) => this.sigma(UnifyTV(x))
-      case UnifyEqualsDot(_, UnifyRefType(n, ps)) => UnifyRefType(n, ps.map(this.sigma(_)))
-      case UnifyLessDot(UnifyTV(x), UnifyRefType(n, ps)) => UnifyTV(x)
-    }
-  }
-}
-
 object Unify {
 
   sealed trait Step4Result{
diff --git a/src/test/scala/IntegrationTest.scala b/src/test/scala/IntegrationTest.scala
index 427437d..aca588b 100644
--- a/src/test/scala/IntegrationTest.scala
+++ b/src/test/scala/IntegrationTest.scala
@@ -6,6 +6,8 @@ class IntegrationTest extends FunSuite {
   test("EmptyClass"){
     val ast = (fastparse.parse(("e.m(a)"), hb.dhbw.Parser.classDefinition(_)))
     //hb.dhbw.TYPE.TYPEClass(ast.get)
+    val result = FJTypeinference.typeinference("class Test extends Object {\n\n}")
+    println(result)
   }
 
   test("IdMethod"){
@@ -64,47 +66,47 @@ class IntegrationTest extends FunSuite {
   test("constructor.FieldInitialization") {
     val input = "class List<A extends Object> extends Object{\nA f;\n  add(a){\n  return new List(a);\n}\n}"
     val result = FJTypeinference.typeinference(input )
-    println(result.map(it => Main.prettyPrintAST(it._2)))
+    println(result.map(it => Main.prettyPrintAST(it)))
   }
   test("list.add") {
     val input = "class List<A extends Object> extends Object{\nA f;\n  add( a){\n  return new List(a);\n}\n}\nclass Test extends Object{\n\nm(a){return a.add(this);}\n}"
     val result = FJTypeinference.typeinference(input )
-    println(result.map(it => Main.prettyPrintAST(it._2)))
+    println(result.map(it => Main.prettyPrintAST(it)))
   }
   test("list.add.2") {
     val input = "class List<A extends Object> extends Object{\n  A head;\n  List<A> tail;\n  add( a){\n  return new List(a, this);\n}\nget(){\nreturn this.head;\n}\n}\n\nclass Test extends Object{\nm(a){\nreturn a.add(this).get();\n}\n}"
     val result = FJTypeinference.typeinference(input )
-    println(result.map(it => Main.prettyPrintAST(it._2)))
+    println(result.map(it => Main.prettyPrintAST(it)))
   }
 
   test("functionClass") {
     val input = "class SameType<A extends Object, B extends Object> extends Object{\nA a;\nA b;\nB c;\nget(){return this.c;}\n}\nclass Function<A extends Object, B extends Object> extends Object{\nA ret;\nB param;\napply(a){\nreturn new SameType(this.param, a, this).get().ret;\n}\n\n}"
     val result = FJTypeinference.typeinference(input )
-    println(result.map(it => Main.prettyPrintAST(it._2)))
+    println(result.map(it => Main.prettyPrintAST(it)))
   }
 
   test("TwoRecursiveMethods") {
     val input = "class RecursiveMethods extends Object{\n\na1(x){ return this.a2(x);}\na2(y){ return this.a1(y);}}"
     val result = FJTypeinference.typeinference(input)
-    println(result.map(it => Main.prettyPrintAST(it._2)))
+    println(result.map(it => Main.prettyPrintAST(it)))
   }
 
   test("Function.typeAnnotaded") {
     val input = "\nclass Function<A extends Object, B extends Object> extends Object{\nB b;\nB apply(A a){\nreturn this.b;\n}\n\n}"
     val result = FJTypeinference.typeinference(input)
-    println(result.map(it => Main.prettyPrintAST(it._2)))
+    println(result.map(it => Main.prettyPrintAST(it)))
   }
 
   test("Box.Map") {
     val input = "class Function<A extends Object, B extends Object> extends Object{\nB b;\nB apply(A a){\nreturn this.b;\n}\n}\n\n\nclass Box<S extends Object> extends Object {\nS val ;\nmap( f ) {\nreturn new Box(f.apply(this.val)) ;\n}\n}"
     val result = FJTypeinference.typeinference(input)
-    println(result.map(it => Main.prettyPrintAST(it._2)))
+    println(result.map(it => Main.prettyPrintAST(it)))
   }
 
   test("PrincipalType") {
     val input = "\nclass List<A extends Object> extends Object{\n  A head;\n  List<A> tail;\n  add( a){\n    return new List(a, this);\n  }\n  get(){\n    return this.head;\n  }\n}\n\nclass PrincipleType extends Object {\n  function(a){\n    return a.add(this).get();\n  }\n}"
     val result = FJTypeinference.typeinference(input)
-    println(result.map(it => Main.prettyPrintAST(it._2)))
+    println(result.map(it => Main.prettyPrintAST(it)))
   }
   /*