diff --git a/src/Model/Type.hs b/src/Model/Type.hs
index e6559bd..872f708 100644
--- a/src/Model/Type.hs
+++ b/src/Model/Type.hs
@@ -51,7 +51,7 @@ data ExplicitExpression = ExplicitEmpty
     | ExplicitFunction {name :: String, args :: [(ExplicitExpression, Coercion)], returnCoercion :: Coercion}
     | ExplicitIfSimple {cond :: (ExplicitExpression, Coercion), block1 :: (ExplicitExpression, Coercion), returnCoercion :: Coercion}
     | ExplicitIfElse {cond :: (ExplicitExpression, Coercion), block1 :: (ExplicitExpression, Coercion), block2 :: (ExplicitExpression, Coercion), returnCoercion :: Coercion}
-    deriving (Show)
+    deriving (Show) 
 
 data TypeCoercion =
     MakeIdCoercion {toType :: Type}
diff --git a/src/PrettyPrinter/Function.hs b/src/PrettyPrinter/Function.hs
index 3115d56..d5cffcc 100644
--- a/src/PrettyPrinter/Function.hs
+++ b/src/PrettyPrinter/Function.hs
@@ -7,6 +7,7 @@ import Model.Function
 import PrettyPrinter.General
 import PrettyPrinter.Type
 import Model.Type
+import Semantic.ExpressionChecker(coercionIncluded)
   
 -- show printStatementTree 
 
@@ -16,36 +17,48 @@ printFunction f = show $ vcat [printFunctionSignature (sign f), printFunctionBod
 
 -- |Converts the body of a Function into a haskell valid Doc
 printFunctionBody :: ExplicitFunction -> Doc a
-printFunctionBody (MakeExplicitFunction (MakeFunctionSignature name _ inp out) ex) = pretty name <+> printVariableNames inp <+> "=" <+> printExpression ex
-printExpression :: ExplicitExpression -> Doc a
-printExpression ExplicitEmpty = "[]" 
-printExpression (ExplicitVariable name coer) = printCoercion coer $ pretty name
-printExpression (Value s coer) = printCoercion coer $ pretty s
-printExpression (ExplicitParens ex) = "(" <> printExpression ex <> ")"
-printExpression (ExplicitList ex) = list (map printExpression ex)
-printExpression (ExplicitFunction "exists" args returnCoerce) = printCoercion returnCoerce "isJust" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args)
-printExpression (ExplicitFunction "is absent" args returnCoerce) = printCoercion returnCoerce "isNothing" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args)
-printExpression (ExplicitFunction "single exists" args returnCoerce) = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "==" <+> "1"
-printExpression (ExplicitFunction "multiple exists" args returnCoerce) = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> ">" <+> "1" 
-printExpression (ExplicitFunction "count" args returnCoerce) = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args)
+printFunctionBody (MakeExplicitFunction (MakeFunctionSignature name _ inp out) ex) = pretty name <+> printVariableNames inp <+> "=" <+> printExpression ex (createCoercion (attributeType out, Model.Type.cardinality out))
+printExpression :: ExplicitExpression -> Coercion -> Doc a
+printExpression ExplicitEmpty _ = "[]" 
+printExpression (ExplicitVariable name coer) out = case coer `coercionIncluded` out of 
+    Left err -> error $ show err
+    Right c -> printCoercion c $ pretty name
+printExpression (Value s coer) out = case coer `coercionIncluded` out of
+    Left err -> error $ show err 
+    Right c -> printCoercion c $ pretty s
+printExpression (ExplicitParens ex) out = "(" <> printExpression ex out <> ")"
+printExpression (ExplicitList ex) out = list [printExpression x out | x <- ex]
+printExpression (ExplicitFunction "exists" args returnCoerce) out = printCoercion returnCoerce "isJust" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out)
+printExpression (ExplicitFunction "is absent" args returnCoerce) out = printCoercion returnCoerce "isNothing" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out)
+printExpression (ExplicitFunction "single exists" args returnCoerce) out = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out) <+> "==" <+> "1"
+printExpression (ExplicitFunction "multiple exists" args returnCoerce) out = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out) <+> ">" <+> "1" 
+printExpression (ExplicitFunction "count" args returnCoerce) out = printCoercion returnCoerce "length" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out)
 -- Equality expressions
 -- [a] a all = 
 -- any <>
-printExpression (ExplicitFunction "=" args returnCoerce) = printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "==" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)
-printExpression (ExplicitFunction "<>" args returnCoerce) = printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "/=" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)
-printExpression (ExplicitFunction "any =" args returnCoerce) = printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)<+> "`elem`" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args)
-printExpression (ExplicitFunction "all <>" args returnCoerce) = printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)<+> "`notElem`" <+> printCoercion (snd $ head args) (printExpression $ fst $ head args)
-printExpression (ExplicitFunction "all =" args returnCoerce) = "all (Eq)" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args) <+> printCoercion (snd $ head args) (printExpression $ fst $ head args)
-printExpression (ExplicitFunction "and" args returnCoerce) = printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "&&" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)
-printExpression (ExplicitFunction "or" args returnCoerce) = printCoercion (snd $ head args) (printExpression $ fst $ head args) <+> "||" <+> printCoercion (snd $ head $ tail args) (printExpression $ fst $ head $ tail args)
-printExpression (ExplicitFunction name args returnCoerce) = pretty name <+> tupled (zipWith printCoercion [c | (e,c) <- args] [printExpression e | (e, c) <- args])
-printExpression (ExplicitIfSimple cond thenBlock returnCoercion) = "if" <+> printCoercion (snd cond) (printExpression $ fst cond) <+> "then" <+> printCoercion (snd thenBlock) (printExpression $ fst thenBlock) <+> "else" <+> "Nothing"
-printExpression (ExplicitIfElse cond thenBlock elseBlock returnCoercion) = "if" <+> printCoercion (snd cond) (printExpression $ fst cond) <+> "then" <+> printCoercion (snd thenBlock) (printExpression $ fst thenBlock) <+> "else" <+> printCoercion (snd elseBlock) (printExpression $ fst elseBlock)
+printExpression (ExplicitFunction "=" args returnCoerce) out = printCoercion (snd $ head args) (printExpression (fst $ head args) out) <+> "==" <+> printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out)
+printExpression (ExplicitFunction "<>" args returnCoerce) out = printCoercion (snd $ head args) (printExpression (fst $ head args) out) <+> "/=" <+> printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out)
+printExpression (ExplicitFunction "any =" args returnCoerce) out = printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out) <+> "`elem`" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out)
+printExpression (ExplicitFunction "all <>" args returnCoerce) out = printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out) <+> "`notElem`" <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out)
+printExpression (ExplicitFunction "all =" args returnCoerce) out = "all (Eq)" <+> printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out) <+> printCoercion (snd $ head args) (printExpression (fst $ head args) out)
+printExpression (ExplicitFunction "and" args returnCoerce) out = printCoercion (snd $ head args) (printExpression (fst $ head args) out) <+> "&&" <+> printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out)
+printExpression (ExplicitFunction "or" args returnCoerce) out = printCoercion (snd $ head args) (printExpression (fst $ head args) out) <+> "||" <+> printCoercion (snd $ head $ tail args) (printExpression (fst $ head $ tail args) out)
+printExpression (ExplicitFunction name args returnCoerce) out = pretty name <+> tupled (zipWith printCoercion [c | (e,c) <- args] [printExpression e out | (e, c) <- args])
+printExpression (ExplicitIfSimple cond thenBlock returnCoercion) out = 
+    "if" <+> printCoercion (snd cond) (printExpression (fst cond) (MakeCoercion [MakeIdCoercion (BasicType "Boolean")] (MakeCardinalityIdCoercion (Bounds (1, 1))))) <+> 
+    "then" <+> printCoercion (snd thenBlock) (printExpression (fst thenBlock) out) <+> 
+    "else" <+> case MakeCoercion [MakeIdCoercion $ coercionType $ typeCoercion returnCoercion] (MakeCardinalityIdCoercion (Bounds (0, 0))) `coercionIncluded` out of
+        Left err -> error $ show err
+        Right c -> printCoercion c emptyDoc
+printExpression (ExplicitIfElse cond thenBlock elseBlock returnCoercion) out = 
+    "if" <+> printCoercion (snd cond) (printExpression (fst cond) (MakeCoercion [MakeIdCoercion (BasicType "Boolean")] (MakeCardinalityIdCoercion (Bounds (1, 1))))) <+> 
+    "then" <+> printCoercion (snd thenBlock) (printExpression (fst thenBlock) out) <+> 
+    "else" <+> printCoercion (snd elseBlock) (printExpression (fst elseBlock) out)
 
 -- |Converts a coercion into a haskell string
 printCoercion :: Coercion -> Doc a -> Doc a
 printCoercion (MakeCoercion [] crd) d = printCardinalityCoercion crd d
-printCoercion (MakeCoercion (t: ts) crd) d = printTypeCoercion t <+> printCoercion (MakeCoercion ts crd) d
+printCoercion (MakeCoercion (t: ts) crd) d = printTypeCoercion t <> printCoercion (MakeCoercion ts crd) d
 
 printCardinalityCoercion :: CardinalityCoercion -> Doc a -> Doc a
 printCardinalityCoercion (MakeCardinalityIdCoercion _) d = d
@@ -58,8 +71,8 @@ printCardinalityCoercion (MakeObject2ListCoercion _ _) d = "[" <> d <> "]"
 
 printTypeCoercion :: TypeCoercion -> Doc a
 printTypeCoercion (MakeIdCoercion _) = emptyDoc
-printTypeCoercion (MakeSuperCoercion _ _) = "super"
-printTypeCoercion (MakeTypeCoercion _ _ t) = pretty t
+printTypeCoercion (MakeSuperCoercion _ _) = "super" <+> emptyDoc
+printTypeCoercion (MakeTypeCoercion _ _ t) = pretty t <+> emptyDoc
 
 -- |Converts a list of type attributes to a Doc with a list of variable names
 printVariableNames :: [TypeAttribute] -> Doc a
diff --git a/src/Semantic/ExpressionChecker.hs b/src/Semantic/ExpressionChecker.hs
index dcc1993..a9b7141 100644
--- a/src/Semantic/ExpressionChecker.hs
+++ b/src/Semantic/ExpressionChecker.hs
@@ -112,8 +112,12 @@ checkExpression symbolMap (IfSimple cond ex) =
                     Left err -> Left err
                     Right thenExp -> 
                         Right $ ExplicitIfSimple (condType, condCoerce) 
-                        (thenExp, MakeCoercion [MakeIdCoercion $ coercionType $ typeCoercion $ returnCoercion thenExp]
-                         (MakeCardinalityIdCoercion $ toCardinality $ cardinalityCoercion $ returnCoercion thenExp)) (returnCoercion thenExp)
+                        (thenExp, thenCoercion) 
+                        (MakeCoercion [MakeIdCoercion $ coercionType $ typeCoercion $ returnCoercion thenExp]
+                            (MakeCardinalityIdCoercion $ smallestBound (Bounds (0, 0)) (toCardinality $ cardinalityCoercion $ returnCoercion thenExp)))
+                        where 
+                            thenCoercion = MakeCoercion [MakeIdCoercion $ coercionType $ typeCoercion $ returnCoercion thenExp] 
+                                (MakeCardinalityIdCoercion $ toCardinality $ cardinalityCoercion $ returnCoercion thenExp)
 
 -- |Checks if the condition of the if statement is of type boolean, and then checks that both the then and else statements have the same type
 checkExpression symbolMap (IfElse cond ex1 ex2) =
@@ -217,13 +221,13 @@ findVarType x (_:symbols) = findVarType x symbols
 isSubType :: Type -> Type -> Either TypeCheckError [TypeCoercion]
 isSubType (BasicType "Integer") (BasicType "Double") = Right [MakeTypeCoercion (BasicType "Integer") (BasicType "Double") "fromInteger"]
 isSubType (BasicType x) y 
-    | x == typeName y = Right [MakeTypeCoercion y y "id"]
+    | x == typeName y = Right [MakeIdCoercion y]
     | otherwise = Left $ TypeMismatch x (typeName y) 
 isSubType x y 
-    | typeName x == typeName y = Right [MakeTypeCoercion x y "id"]
+    | typeName x == typeName y = Right [MakeIdCoercion x]
     | otherwise = case isSubType (superType x) y of
         Left e -> Left e
-        Right transforms -> Right $ MakeTypeCoercion x y "super" : transforms
+        Right transforms -> Right $ MakeSuperCoercion x y : transforms
 
 -- |Checks whether the first cardinality is included into the second one 
 cardinalityIncluded :: Cardinality -> Cardinality -> Either TypeCheckError CardinalityCoercion
@@ -238,6 +242,7 @@ cardinalityIncluded (Bounds (0, 1)) (OneBound 0) = Right $ MakeMaybe2ListCoercio
 cardinalityIncluded (Bounds (1, 1)) (Bounds (0, 1)) = Right $ MakeObject2MaybeCoercion (Bounds (0, 1)) (Bounds (0, 1))
 -- |Transform object into list
 cardinalityIncluded (Bounds (1, 1)) (OneBound 1) = Right $ MakeObject2ListCoercion (Bounds (0, 1)) (OneBound 1)
+cardinalityIncluded (Bounds (1, 1)) (OneBound 0) = Right $ MakeObject2ListCoercion (Bounds (0, 1)) (OneBound 1)
 -- |General
 cardinalityIncluded (OneBound x) (OneBound y)
     | x >= y = Right $ MakeListCardinalityCoercion (OneBound x) (OneBound y)
diff --git a/src/Semantic/FunctionChecker.hs b/src/Semantic/FunctionChecker.hs
index 5f90c60..141d2e5 100644
--- a/src/Semantic/FunctionChecker.hs
+++ b/src/Semantic/FunctionChecker.hs
@@ -19,7 +19,8 @@ checkFunction (definedTypes, symbols) (MakeFunction (MakeFunctionSignature name
                     Left err -> Left [err]
                     Right checkedEx -> case returnCoercion checkedEx `coercionIncluded` createCoercion (attributeType checkedOut, Model.Type.cardinality out) of
                         Left err -> Left [err]
-                        Right _ -> Right $ MakeExplicitFunction (MakeFunctionSignature (toLower (head name) : tail name) desc (rights checkedIn) checkedOut) checkedEx
+                        Right retCoercion -> Right $ MakeExplicitFunction (MakeFunctionSignature (toLower (head name) : tail name) desc (rights checkedIn) checkedOut) checkedEx
+                        --Right _ -> error $ show (returnCoercion checkedEx) ++ " // " ++ show (createCoercion (attributeType checkedOut, Model.Type.cardinality out))
         else
             Left $ lefts checkedIn
     where checkedIn = checkAttributes definedTypes inp
\ No newline at end of file