diff --git a/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java b/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java
index 1c75ea99..aa5f6ddd 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/MartelliMontanariUnify.java
@@ -94,7 +94,8 @@ public class MartelliMontanariUnify implements IUnify {
 			// SUBST - Rule
 			if(lhsType instanceof PlaceholderType) {
 				mgu.add((PlaceholderType) lhsType, rhsType);
-				termsList = termsList.stream().map(mgu::apply).collect(Collectors.toCollection(ArrayList::new));
+				//PL 2018-04-01 nach checken, ob es richtig ist, dass keine Substitutionen uebergeben werden muessen. 
+				termsList = termsList.stream().map(x -> mgu.apply(new HashSet<>(), x)).collect(Collectors.toCollection(ArrayList::new));
 				idx = idx+1 == termsList.size() ? 0 : idx+1;
 				continue;
 			}
diff --git a/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java b/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java
index 660ab38c..62473eff 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/RuleSet.java
@@ -60,7 +60,7 @@ public class RuleSet implements IRuleSet{
 			return Optional.empty();
 		
 		// Rule is applicable, unpack the SuperType 
-		return Optional.of(new UnifyPair(lhsType, ((SuperType) rhsType).getSuperedType(), PairOperator.SMALLERDOT));
+		return Optional.of(new UnifyPair(lhsType, ((SuperType) rhsType).getSuperedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
 	}
 
 	@Override
@@ -78,7 +78,7 @@ public class RuleSet implements IRuleSet{
 			return Optional.empty();
 
 		// Rule is applicable, unpack the ExtendsType
-		return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(), rhsType, PairOperator.SMALLERDOT));
+		return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(), rhsType, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
 	}
 
 	@Override
@@ -96,7 +96,7 @@ public class RuleSet implements IRuleSet{
 			return Optional.empty();
 		
 		// Rule is applicable, unpack both sides
-		return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(),((SuperType) rhsType).getSuperedType(), PairOperator.SMALLERDOT));
+		return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(),((SuperType) rhsType).getSuperedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
 	}
 
 	@Override
@@ -146,7 +146,7 @@ public class RuleSet implements IRuleSet{
 		Set<UnifyPair> result = new HashSet<>();
 		
 		for(int rhsIdx = 0; rhsIdx < extYParams.size(); rhsIdx++)
-			result.add(new UnifyPair(xParams.get(pi[rhsIdx]), extYParams.get(rhsIdx), PairOperator.SMALLERDOTWC));
+			result.add(new UnifyPair(xParams.get(pi[rhsIdx]), extYParams.get(rhsIdx), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
 		
 		return Optional.of(result);
 	}
@@ -197,7 +197,7 @@ public class RuleSet implements IRuleSet{
 			return Optional.empty();
 		
 		for(int rhsIdx = 0; rhsIdx < supYParams.size(); rhsIdx++)
-			result.add(new UnifyPair(supYParams.get(rhsIdx), xParams.get(pi[rhsIdx]), PairOperator.SMALLERDOTWC));
+			result.add(new UnifyPair(supYParams.get(rhsIdx), xParams.get(pi[rhsIdx]), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
 		
 		return Optional.of(result);
 	}
@@ -228,7 +228,7 @@ public class RuleSet implements IRuleSet{
 		TypeParams rhsTypeParams = rhsType.getTypeParams();
 		
 		for(int i = 0; i < lhsTypeParams.size(); i++)
-			result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT));
+			result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
 		
 		return Optional.of(result);
 	}
@@ -269,7 +269,7 @@ public class RuleSet implements IRuleSet{
 			TypeParams rhsTypeParams = d.getTypeParams();
 			TypeParams lhsTypeParams = c.getTypeParams();
 			for(int rhsIdx = 0; rhsIdx < c.getTypeParams().size(); rhsIdx++)
-				result.add(new UnifyPair(lhsTypeParams.get(rhsIdx), rhsTypeParams.get(rhsIdx), PairOperator.SMALLERDOTWC));
+				result.add(new UnifyPair(lhsTypeParams.get(rhsIdx), rhsTypeParams.get(rhsIdx), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
 		
 			return Optional.of(result);
 		}
@@ -306,7 +306,7 @@ public class RuleSet implements IRuleSet{
 		Set<UnifyPair> result = new HashSet<>();
 		
 		for(int rhsIdx = 0; rhsIdx < rhsTypeParams.size(); rhsIdx++)
-			result.add(new UnifyPair(lhsTypeParams.get(pi[rhsIdx]), rhsTypeParams.get(rhsIdx), PairOperator.SMALLERDOTWC));
+			result.add(new UnifyPair(lhsTypeParams.get(pi[rhsIdx]), rhsTypeParams.get(rhsIdx), PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
 		
 		return Optional.of(result);
 	}
@@ -361,7 +361,7 @@ public class RuleSet implements IRuleSet{
 		TypeParams rhsTypeParams = rhsSType.getTypeParams();
 		TypeParams lhsTypeParams = lhsSType.getTypeParams();
 		for(int i = 0; i < rhsTypeParams.size(); i++)
-			result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT));
+			result.add(new UnifyPair(lhsTypeParams.get(i), rhsTypeParams.get(i), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
 		
 		return Optional.of(result);
 	}
@@ -412,7 +412,7 @@ public class RuleSet implements IRuleSet{
 		if(!(pair.getRhsType() instanceof PlaceholderType))
 			return Optional.empty();
 		
-		return Optional.of(new UnifyPair(pair.getRhsType(), pair.getLhsType(), PairOperator.EQUALSDOT));
+		return Optional.of(new UnifyPair(pair.getRhsType(), pair.getLhsType(), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
 	}
 
 	@Override
@@ -466,7 +466,7 @@ public class RuleSet implements IRuleSet{
 			unif.add((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i));
 			else System.out.println("ERROR");
 		}
-		return Optional.of(new UnifyPair(unif.apply(newLhs), typeDs, PairOperator.SMALLERDOT));
+		return Optional.of(new UnifyPair(unif.apply(newLhs), typeDs, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
 	}
 
 	@Override
@@ -512,7 +512,7 @@ public class RuleSet implements IRuleSet{
 		for(int i = 1; i < typeDParams.size(); i++) 
 			unif.add((PlaceholderType) typeDgenParams.get(i), typeDParams.get(i));
 		
-		return Optional.of(new UnifyPair(unif.apply(newLhs), typeExtDs, PairOperator.SMALLERDOTWC));
+		return Optional.of(new UnifyPair(unif.apply(newLhs), typeExtDs, PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
 	}
 
 	@Override
@@ -564,7 +564,7 @@ public class RuleSet implements IRuleSet{
 		for(int i = 1; i < typeDParams.size(); i++) 
 			unif.add((PlaceholderType) typeSupDsgenParams.get(i), typeDParams.get(i));
 		
-		return Optional.of(new UnifyPair(unif.apply(newLhs), newRhs, PairOperator.SMALLERDOTWC));
+		return Optional.of(new UnifyPair(unif.apply(newLhs), newRhs, PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
 	}
 
 	/**
@@ -636,8 +636,8 @@ public class RuleSet implements IRuleSet{
 					&& typeMap.get(lhsType) > 1  // The type occurs in more pairs in the set than just the recent pair.
 					&& !rhsType.getTypeParams().occurs(lhsType)) {
 				Unifier uni = new Unifier(lhsType,  rhsType);
-				result = result.stream().map(uni::apply).collect(Collectors.toCollection(ArrayList::new));
-				result1 = result1.stream().map(uni::apply).collect(Collectors.toCollection(LinkedList::new));
+				result = result.stream().map(x -> uni.apply(pair.getSubstitution(),x)).collect(Collectors.toCollection(ArrayList::new));
+				result1 = result1.stream().map(x -> uni.apply(pair.getSubstitution(),x)).collect(Collectors.toCollection(LinkedList::new));
 				applied = true;
 			}
 			
@@ -657,7 +657,7 @@ public class RuleSet implements IRuleSet{
 		if(!(lhsType instanceof ExtendsType) || !(rhsType instanceof ExtendsType))
 			return Optional.empty();
 		
-		return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(), ((ExtendsType) rhsType).getExtendedType(), PairOperator.SMALLERDOT)); 
+		return Optional.of(new UnifyPair(((ExtendsType) lhsType).getExtendedType(), ((ExtendsType) rhsType).getExtendedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair())); 
 	}
 
 	@Override
@@ -670,7 +670,7 @@ public class RuleSet implements IRuleSet{
 		if(!(lhsType instanceof ReferenceType) || !(rhsType instanceof ExtendsType))
 			return Optional.empty();
 		
-		return Optional.of(new UnifyPair(lhsType, ((ExtendsType) rhsType).getExtendedType(), PairOperator.SMALLERDOT));
+		return Optional.of(new UnifyPair(lhsType, ((ExtendsType) rhsType).getExtendedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
 	}
 
 	@Override
@@ -683,7 +683,7 @@ public class RuleSet implements IRuleSet{
 		if(!(lhsType instanceof SuperType) || !(rhsType instanceof SuperType))
 			return Optional.empty();
 		
-		return Optional.of(new UnifyPair(((SuperType) rhsType).getSuperedType(), ((SuperType) lhsType).getSuperedType(), PairOperator.SMALLERDOT));
+		return Optional.of(new UnifyPair(((SuperType) rhsType).getSuperedType(), ((SuperType) lhsType).getSuperedType(), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
 	}
 
 	@Override
@@ -696,7 +696,7 @@ public class RuleSet implements IRuleSet{
 		if(!(lhsType instanceof ReferenceType) || !(rhsType instanceof SuperType))
 			return Optional.empty();
 		
-		return Optional.of(new UnifyPair(((SuperType) rhsType).getSuperedType(), lhsType, PairOperator.SMALLERDOTWC));
+		return Optional.of(new UnifyPair(((SuperType) rhsType).getSuperedType(), lhsType, PairOperator.SMALLERDOTWC, pair.getSubstitution(), pair.getBasePair()));
 	}
 
 	/* PL 2018-03-06 auskommentiert sind mutmaßlich falsch
@@ -767,9 +767,9 @@ public class RuleSet implements IRuleSet{
 		
 		Set<UnifyPair> result = new HashSet<UnifyPair>();
 		
-		result.add(new UnifyPair(funNLhsType.getTypeParams().get(0), funNRhsType.getTypeParams().get(0), PairOperator.SMALLERDOT));
+		result.add(new UnifyPair(funNLhsType.getTypeParams().get(0), funNRhsType.getTypeParams().get(0), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
 		for(int i = 1; i < funNLhsType.getTypeParams().size(); i++)
-			result.add(new UnifyPair(funNRhsType.getTypeParams().get(i), funNLhsType.getTypeParams().get(i), PairOperator.SMALLERDOT));
+			result.add(new UnifyPair(funNRhsType.getTypeParams().get(i), funNLhsType.getTypeParams().get(i), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
 		
 		return Optional.of(result);
 	}
@@ -793,10 +793,10 @@ public class RuleSet implements IRuleSet{
 		for(int i = 0; i < freshPlaceholders.length; i++)
 			freshPlaceholders[i] = PlaceholderType.freshPlaceholder();
 		
-		result.add(new UnifyPair(funNLhsType.getTypeParams().get(0), freshPlaceholders[0], PairOperator.SMALLERDOT));
+		result.add(new UnifyPair(funNLhsType.getTypeParams().get(0), freshPlaceholders[0], PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
 		for(int i = 1; i < funNLhsType.getTypeParams().size(); i++)
-			result.add(new UnifyPair(freshPlaceholders[i], funNLhsType.getTypeParams().get(i), PairOperator.SMALLERDOT));
-		result.add(new UnifyPair(rhsType, funNLhsType.setTypeParams(new TypeParams(freshPlaceholders)), PairOperator.EQUALSDOT));
+			result.add(new UnifyPair(freshPlaceholders[i], funNLhsType.getTypeParams().get(i), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
+		result.add(new UnifyPair(rhsType, funNLhsType.setTypeParams(new TypeParams(freshPlaceholders)), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
 		
 		return Optional.of(result);
 	}
@@ -820,10 +820,10 @@ public class RuleSet implements IRuleSet{
 		for(int i = 0; i < freshPlaceholders.length; i++)
 			freshPlaceholders[i] = PlaceholderType.freshPlaceholder();
 		
-		result.add(new UnifyPair(freshPlaceholders[0], funNRhsType.getTypeParams().get(0), PairOperator.SMALLERDOT));
+		result.add(new UnifyPair(freshPlaceholders[0], funNRhsType.getTypeParams().get(0), PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
 		for(int i = 1; i < funNRhsType.getTypeParams().size(); i++)
-			result.add(new UnifyPair(funNRhsType.getTypeParams().get(i), freshPlaceholders[i], PairOperator.SMALLERDOT));
-		result.add(new UnifyPair(lhsType, funNRhsType.setTypeParams(new TypeParams(freshPlaceholders)), PairOperator.EQUALSDOT));
+			result.add(new UnifyPair(funNRhsType.getTypeParams().get(i), freshPlaceholders[i], PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
+		result.add(new UnifyPair(lhsType, funNRhsType.setTypeParams(new TypeParams(freshPlaceholders)), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
 		
 		return Optional.of(result);
 	}
@@ -838,7 +838,7 @@ public class RuleSet implements IRuleSet{
 		if(!(lhsType instanceof PlaceholderType) || !(rhsType instanceof ReferenceType))
 			return Optional.empty();
 		
-		return Optional.of(new UnifyPair(lhsType, rhsType, PairOperator.EQUALSDOT));
+		return Optional.of(new UnifyPair(lhsType, rhsType, PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
 	}
 
 	@Override
@@ -857,11 +857,11 @@ public class RuleSet implements IRuleSet{
 		
 		Set<UnifyPair> result = new HashSet<>();
 		if(isGen)
-			result.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT));
+			result.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
 		else {
 			UnifyType freshTph = PlaceholderType.freshPlaceholder();
-			result.add(new UnifyPair(rhsType, new ExtendsType(freshTph), PairOperator.EQUALSDOT));
-			result.add(new UnifyPair(extendedType, freshTph, PairOperator.SMALLERDOT));
+			result.add(new UnifyPair(rhsType, new ExtendsType(freshTph), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
+			result.add(new UnifyPair(extendedType, freshTph, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
 		}
 		
 		return Optional.of(result);
@@ -883,11 +883,11 @@ public class RuleSet implements IRuleSet{
 		
 		Set<UnifyPair> result = new HashSet<>();
 		if(isGen)
-			result.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT));
+			result.add(new UnifyPair(rhsType, lhsType, PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
 		else {
 			UnifyType freshTph = PlaceholderType.freshPlaceholder();
-			result.add(new UnifyPair(rhsType, new SuperType(freshTph), PairOperator.EQUALSDOT));
-			result.add(new UnifyPair(freshTph, superedType, PairOperator.SMALLERDOT));
+			result.add(new UnifyPair(rhsType, new SuperType(freshTph), PairOperator.EQUALSDOT, pair.getSubstitution(), pair.getBasePair()));
+			result.add(new UnifyPair(freshTph, superedType, PairOperator.SMALLERDOT, pair.getSubstitution(), pair.getBasePair()));
 		}
 		
 		return Optional.of(result);
diff --git a/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
index 81c6da3a..c988d35f 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/TypeUnifyTask.java
@@ -644,7 +644,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			if(pairOp == PairOperator.SMALLERDOT && lhsType instanceof PlaceholderType) {
 				//System.out.println(pair);
 				if (first) { //writeLog(pair.toString()+"\n");
-					Set<Set<UnifyPair>> x1 = unifyCase1((PlaceholderType) pair.getLhsType(), pair.getRhsType(), pair.getVariance(), fc);
+					Set<Set<UnifyPair>> x1 = unifyCase1(pair, fc);
 				//System.out.println(x1);
 					result.get(0).add(x1);
 				}
@@ -660,7 +660,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			// Case 2: (a <.? ? ext Theta')
 			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof ExtendsType)
 				if (first) { //writeLog(pair.toString()+"\n");
-					result.get(1).add(unifyCase2((PlaceholderType) pair.getLhsType(), (ExtendsType) pair.getRhsType(), pair.getVariance(), fc));
+					result.get(1).add(unifyCase2(pair, fc));
 				}	
 				else {
 					Set<UnifyPair> s1 = new HashSet<>();
@@ -673,7 +673,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			// Case 3: (a <.? ? sup Theta')
 			else if(pairOp == PairOperator.SMALLERDOTWC && lhsType instanceof PlaceholderType && rhsType instanceof SuperType)
 				if (first) { //writeLog(pair.toString()+"\n");
-					result.get(2).add(unifyCase3((PlaceholderType) lhsType, (SuperType) rhsType, pair.getVariance(), fc));
+					result.get(2).add(unifyCase3(pair, fc));
 				}
 				else {
 					Set<UnifyPair> s1 = new HashSet<>();
@@ -693,7 +693,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 				if (first) { //writeLog(pair.toString()+"\n");
 					if (rhsType.getName().equals("A")) 
 						System.out.println();
-					result.get(4).add(unifyCase5(lhsType, (PlaceholderType) rhsType, pair.getVariance(), fc));
+					result.get(4).add(unifyCase5(pair, fc));
 				}
 				else {
 					Set<UnifyPair> s1 = new HashSet<>();
@@ -717,7 +717,7 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 			else if(pairOp == PairOperator.SMALLERDOTWC && rhsType instanceof PlaceholderType)
 				if (first) { //writeLog(pair.toString()+"\n");
 					result.get(7).add(
-							unifyCase8(lhsType, (PlaceholderType) rhsType, pair.getVariance(), fc));
+							unifyCase8(pair, fc));
 				}
 				else {
 					Set<UnifyPair> s1 = new HashSet<>();
@@ -745,7 +745,10 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	/**
 	 * Cartesian product Case 1: (a <. Theta') 
 	 */
-	protected Set<Set<UnifyPair>> unifyCase1(PlaceholderType a, UnifyType thetaPrime, byte variance, IFiniteClosure fc) {
+	protected Set<Set<UnifyPair>> unifyCase1(UnifyPair pair, IFiniteClosure fc) {
+		PlaceholderType a = (PlaceholderType)pair.getLhsType(); 
+		UnifyType thetaPrime = pair.getRhsType(); 
+		byte variance = pair.getVariance();
 		if (a.getName().equals("D")) {
 			System.out.print("");
 		}
@@ -865,7 +868,10 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	/**
 	 * Cartesian Product Case 2: (a <.? ? ext Theta')
 	 */
-	private Set<Set<UnifyPair>> unifyCase2(PlaceholderType a, ExtendsType extThetaPrime, byte variance, IFiniteClosure fc) {
+	private Set<Set<UnifyPair>> unifyCase2(UnifyPair pair, IFiniteClosure fc) {
+		PlaceholderType a = (PlaceholderType) pair.getLhsType();
+		ExtendsType extThetaPrime = (ExtendsType) pair.getRhsType();
+		byte variance = pair.getVariance();
 		Set<Set<UnifyPair>> result = new HashSet<>();
 		
 		UnifyType aPrime = PlaceholderType.freshPlaceholder();
@@ -887,7 +893,10 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	/**
 	 * Cartesian Product Case 3: (a <.? ? sup Theta')
 	 */
-	private Set<Set<UnifyPair>> unifyCase3(PlaceholderType a, SuperType subThetaPrime, byte variance, IFiniteClosure fc) {
+	private Set<Set<UnifyPair>> unifyCase3(UnifyPair pair, IFiniteClosure fc) {
+		PlaceholderType a = (PlaceholderType) pair.getLhsType();
+		SuperType subThetaPrime = (SuperType) pair.getRhsType();
+		byte variance = pair.getVariance();
 		Set<Set<UnifyPair>> result = new HashSet<>();
 		
 		UnifyType aPrime = PlaceholderType.freshPlaceholder();
@@ -911,7 +920,10 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	/**
 	 * Cartesian Product Case 5: (Theta <. a)
 	 */
-	private Set<Set<UnifyPair>> unifyCase5(UnifyType theta, PlaceholderType a, byte variance, IFiniteClosure fc) {
+	private Set<Set<UnifyPair>> unifyCase5(UnifyPair pair, IFiniteClosure fc) {
+		UnifyType theta = pair.getLhsType();
+		PlaceholderType a = (PlaceholderType) pair.getRhsType();
+		byte variance = pair.getVariance();
 		Set<Set<UnifyPair>> result = new HashSet<>();
 		
 		boolean allGen = theta.getTypeParams().size() > 0;
@@ -945,7 +957,10 @@ public class TypeUnifyTask extends RecursiveTask<Set<Set<UnifyPair>>>  {
 	/**
 	 * Cartesian Product Case 8: (Theta <.? a)
 	 */
-	private Set<Set<UnifyPair>> unifyCase8(UnifyType theta, PlaceholderType a, byte variance, IFiniteClosure fc) {
+	private Set<Set<UnifyPair>> unifyCase8(UnifyPair pair, IFiniteClosure fc) {
+		UnifyType theta = pair.getLhsType();
+	    PlaceholderType a = (PlaceholderType) pair.getRhsType();
+	    byte variance = pair.getVariance();
 		Set<Set<UnifyPair>> result = new HashSet<>();
 		//for(UnifyType thetaS : fc.grArg(theta)) {
 		Set<UnifyPair> resultPrime = new HashSet<>();
diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/OrderingUnifyPair.java b/src/de/dhbwstuttgart/typeinference/unify/model/OrderingUnifyPair.java
index 12943305..e9896667 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/model/OrderingUnifyPair.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/model/OrderingUnifyPair.java
@@ -151,8 +151,8 @@ public class OrderingUnifyPair extends Ordering<Set<UnifyPair>> {
 				if (!lseq.getRhsType().getName().equals(rseq.getRhsType().getName()) 
 					|| leftlewc.size() == 0 || rightlewc.size() == 0) return int_Unifier.getKey();
 				else {
-					Set <UnifyPair> lsleuni = leftlewc.stream().map(uni::apply).collect(Collectors.toCollection(HashSet::new));
-					Set <UnifyPair> rsleuni = rightlewc.stream().map(uni::apply).collect(Collectors.toCollection(HashSet::new));
+					Set <UnifyPair> lsleuni = leftlewc.stream().map(x -> uni.apply(new HashSet<>(),x)).collect(Collectors.toCollection(HashSet::new));
+					Set <UnifyPair> rsleuni = rightlewc.stream().map(x -> uni.apply(new HashSet<>(),x)).collect(Collectors.toCollection(HashSet::new));
 					BinaryOperator<HashMap<UnifyType,UnifyPair>> combiner = (x,y) -> { x.putAll(y); return x;};
 				
 					HashMap<UnifyType,UnifyPair> hm;
@@ -183,7 +183,7 @@ public class OrderingUnifyPair extends Ordering<Set<UnifyPair>> {
 					}
 					Unifier uni = new Unifier();
 					subst.stream().forEach(x -> uni.add((PlaceholderType) x.getLhsType(), x.getRhsType()));
-					lseq = uni.apply(lseq);
+					lseq = uni.apply(new HashSet<>(), lseq);
 				}
 				else {
 					Set<UnifyPair> subst;
@@ -195,7 +195,7 @@ public class OrderingUnifyPair extends Ordering<Set<UnifyPair>> {
 					}
 					Unifier uni = new Unifier();
 					subst.stream().forEach(x -> uni.add((PlaceholderType) x.getLhsType(), x.getRhsType()));
-					rseq = uni.apply(rseq);
+					rseq = uni.apply(new HashSet<>(), rseq);
 				}
 				return compareEq(lseq, rseq);
 			}
diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java
index 1ee05264..d9b31e24 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/model/Unifier.java
@@ -1,8 +1,10 @@
 package de.dhbwstuttgart.typeinference.unify.model;
 
 import java.util.HashMap;
+import java.util.HashSet;
 import java.util.Iterator;
 import java.util.Map.Entry;
+import java.util.Set;
 import java.util.function.Function;
 
 /**
@@ -62,11 +64,14 @@ public class Unifier implements Function<UnifyType, UnifyType>, Iterable<Entry<P
 	 * Applies the unifier to the two terms of the pair.
 	 * @return A new pair where the left and right-hand side are applied
 	 */
-	public UnifyPair apply(UnifyPair p) {
+	public UnifyPair apply(Set<Unifier> suniSubstitution, UnifyPair p) {
 		UnifyType newLhs = this.apply(p.getLhsType());
 		UnifyType newRhs = this.apply(p.getRhsType());
 		if (!(p.getLhsType().equals(newLhs)) || !(p.getRhsType().equals(newRhs))) {//Die Anwedung von this hat was veraendert PL 2018-04-01
-			return new UnifyPair(newLhs, newRhs, p.getPairOp(), this, p);
+			Set<Unifier> suniUnifyPair = new HashSet<>();
+			suniUnifyPair.addAll(suniSubstitution);
+			suniUnifyPair.add(this);
+			return new UnifyPair(newLhs, newRhs, p.getPairOp(), suniUnifyPair, p);
 		}
 		return new UnifyPair(newLhs, newRhs, p.getPairOp(), p.getSubstitution(), p.getBasePair());
 	}
diff --git a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java
index 173b5f8c..11d11ba1 100644
--- a/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java
+++ b/src/de/dhbwstuttgart/typeinference/unify/model/UnifyPair.java
@@ -2,7 +2,9 @@ package de.dhbwstuttgart.typeinference.unify.model;
 
 import java.util.ArrayList;
 import java.util.Collection;
+import java.util.HashSet;
 import java.util.List;
+import java.util.Set;
 
 
 /**
@@ -41,7 +43,7 @@ public class UnifyPair {
      * Unifier/substitute that generated this pair
      * PL 2018-03-15
      */
-    private Unifier substitution;
+    private Set<Unifier> substitution;
     
     /**
      * Base on which the the unifier is applied
@@ -61,12 +63,13 @@ public class UnifyPair {
 		this.lhs = lhs;
 		this.rhs = rhs;
 		pairOp = op;
+		substitution = new HashSet<>();
 		
 		// Caching hashcode
 		hashCode = 17 + 31 * lhs.hashCode() + 31 * rhs.hashCode() + 31 * pairOp.hashCode();
 	}	
 	
-	public UnifyPair(UnifyType lhs, UnifyType rhs, PairOperator op, Unifier uni, UnifyPair base) {
+	public UnifyPair(UnifyType lhs, UnifyType rhs, PairOperator op, Set<Unifier> uni, UnifyPair base) {
 		this.lhs = lhs;
 		this.rhs = rhs;
 		pairOp = op;
@@ -111,7 +114,7 @@ public class UnifyPair {
 	public void setUndefinedPair() {
 		undefinedPair = true;
 	}
-	public Unifier getSubstitution() {
+	public Set<Unifier> getSubstitution() {
 		return substitution;
 	}