diff --git a/src/main/scala/inox/ast/SymbolOps.scala b/src/main/scala/inox/ast/SymbolOps.scala
index 9e170a10a78fd117d48641499177bc55d1c7ca56..f78c4060c48f24b70b332f78468ce9fcd94743b4 100644
--- a/src/main/scala/inox/ast/SymbolOps.scala
+++ b/src/main/scala/inox/ast/SymbolOps.scala
@@ -330,31 +330,20 @@ trait SymbolOps { self: TypeOps =>
   }
 
   private def hasInstance(tadt: TypedADTDefinition): Boolean = {
-    val recursive = Set(tadt, tadt.root)
-
-    def isRecursive(tpe: Type, seen: Set[TypedADTDefinition]): Boolean = tpe match {
-      case adt: ADTType =>
-        val tadt = adt.getADT
-        if (seen(tadt)) {
-          false
-        } else if (recursive(tadt)) {
-          true
-        } else tadt match {
-          case tcons: TypedADTConstructor =>
-            tcons.fieldsTypes.exists(isRecursive(_, seen + tadt))
-          case _ => false
-        }
-      case _ => false
-    }
+    def rec(adt: TypedADTDefinition, seen: Set[TypedADTDefinition]): Boolean = {
+      if (seen(adt)) false else (adt match {
+        case tsort: TypedADTSort =>
+          tsort.constructors.exists(rec(_, seen + tsort))
 
-    val tconss = tadt match {
-      case tsort: TypedADTSort => tsort.constructors
-      case tcons: TypedADTConstructor => Seq(tcons)
+        case tcons: TypedADTConstructor =>
+          tcons.fieldsTypes.flatMap(tpe => typeOps.collect {
+            case t: ADTType => Set(t.getADT)
+            case _ => Set.empty[TypedADTDefinition]
+          } (tpe)).forall(rec(_, seen + tcons))
+      })
     }
 
-    tconss.exists { tcons =>
-      tcons.fieldsTypes.forall(tpe => !isRecursive(tpe, Set.empty))
-    }
+    rec(tadt, Set.empty)
   }
 
   /** Returns simplest value of a given type */
diff --git a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
index fa4c0f6f173f3bc8e6b51657764a5a796b612529..2fc373f6586eb0caa5b8f825660bbc4a7456f821 100644
--- a/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
+++ b/src/main/scala/inox/solvers/unrolling/TemplateGenerator.scala
@@ -339,7 +339,7 @@ trait TemplateGenerator { self: Templates =>
           depConds, depExprs, depTree, depClauses, depCalls, depApps, depMatchers, depLambdas, depQuants)
 
         val realLambda = if (isNormalForm) l else struct
-        val lid = Variable(FreshIdentifier("lambda", true), bestRealType(l.getType))
+        val lid = Variable(FreshIdentifier("lambda", true), l.getType)
         val clauses = liftedEquals(lid, realLambda, idArgs, inlineFirst = true)
 
         val clauseSubst: Map[Variable, Encoded] = depSubst ++ (idArgs zip trArgs)