diff --git a/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSL.scala b/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSL.scala
index cdfb344..c14412d 100644
--- a/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSL.scala
+++ b/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSL.scala
@@ -38,14 +38,7 @@ object GenerativeFluentAssertionsDSL:
     import quotes.reflect.*
 
     property match
-      case '{ (${ typeProvider }: HavePropertyTypeProvider[subjectType])
-        .applyDynamic($propertyNameExpr: String)(satisfying)
-        .$asInstanceOf$[SatisfyingNotEquals[T]] } => '{
-        $typeProvider
-          .applyDynamic($propertyNameExpr)(satisfying.notEquals[T]($obj, $ord))
-          .$asInstanceOf$[AssertionProperty]
-      }
-      case '{ (${ typeProvider }: ContainsPropertyTypeProvider[subjectType])
+      case '{ (${ typeProvider }: HavePropertyTypeProvider[subjectType, elemType])
         .applyDynamic($propertyNameExpr: String)(satisfying)
         .$asInstanceOf$[SatisfyingNotEquals[T]] } => '{
         $typeProvider
@@ -127,18 +120,19 @@ object GenerativeFluentAssertionsDSL:
       // The quoted pattern also extracts: the type of the assertion subject,
       // and the type of the property (actually... not exactly that. Why?)
       case '{
-            (${ typeProvider }: HavePropertyTypeProvider[subjectType])
+            (${ typeProvider }: HavePropertyTypeProvider[subjectType, elemType])
               .applyDynamic($propertyNameExpr: String)($valueExpr: Condition[valueType])
               .$asInstanceOf$[AssertionProperty]
           } =>
-        val subjectExpr = '{ $typeProvider.subject }
-        val negatedExpr = '{ $typeProvider.negated }
-        generateShouldHaveAssertion[subjectType, valueType](
-          subjectExpr,
-          propertyNameExpr,
-          valueExpr,
-          negatedExpr
-        )
+        '{}
+//        val subjectExpr = '{ $typeProvider.subject }
+//        val negatedExpr = '{ $typeProvider.negated }
+//        generateShouldHaveAssertion[subjectType, valueType](
+//          subjectExpr,
+//          propertyNameExpr,
+//          valueExpr,
+//          negatedExpr
+//        )
       case '{
             (${ typeProvider }: BePropertyTypeProvider[subjectType])
               .applyDynamic($propertyNameExpr)($unit)
@@ -151,14 +145,7 @@ object GenerativeFluentAssertionsDSL:
           .$asInstanceOf$[AssertionProperty]
       } =>
         '{} // placeholder
-      case '{
-        (${ typeProvider }: ContainsPropertyTypeProvider[subjectType])
-          .applyDynamic($propertyNameExpr: String)($valueExpr: Condition[valueType])
-          .$asInstanceOf$[AssertionProperty]
-      } =>
-        '{} // placeholder
       case a =>
-        println(a.show)
         report.errorAndAbort(
           "Invalid expression, must be a 'should be' or 'should have' assertion. ",
           assertionExpr
@@ -224,22 +211,7 @@ object GenerativeFluentAssertionsDSL:
       )
     else
       val candidateMethod = optionalCandidateSymbol.get
-      /*
-       * This version is slightly different than the one presented during
-       * the lecture. In this case we also generate a proper message for
-       * the assertion violation, so we need to declare and reuse a local
-       * variable, otherwise the same expression with the type provider needs
-       * to be duplicated and inserted multiple times. So we take the subjectExpr,
-       * which contains the type provider and selects the subject, and we
-       * save it to a local val 'subject'. Then we use the low-level AST
-       * API to retrieve the result:
-       * first we take '(subject), which is the expression corresponding
-       * to the subject variable, and we take the low-level term version;
-       * then, we construct the Select AST which corresponds to the method
-       * invocation;
-       * finally, we convert all to an expression back again, which can be
-       * spliced in the quote.
-       */
+
       val assertion = '{
         val subject = $subjectExpr
         val negated = $negatedExpr
@@ -248,7 +220,7 @@ object GenerativeFluentAssertionsDSL:
 
         assert(
           condition.test(value) == !negated,
-          s"${subject}.${$propertyNameExpr} " + condition.failedMessage(negated) + " but " + value
+          s"$subject.${$propertyNameExpr} " + condition.failedMessage(negated) + " but " + value
         )
       }
       report.info(assertion.show, subjectExpr.asTerm.pos)
diff --git a/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSLSyntax.scala b/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSLSyntax.scala
index 7d586f2..583bf02 100644
--- a/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSLSyntax.scala
+++ b/src/main/scala/ch/usi/si/msde/edsl/lecture10/GenerativeFluentAssertionsDSLSyntax.scala
@@ -38,21 +38,35 @@ class BePropertyTypeProvider[T](val subject: T) extends Selectable:
   def applyDynamic(fieldName: String)(foo: Any*): AssertionProperty = ???
 end BePropertyTypeProvider
 
-class HavePropertyTypeProvider[T](val subject: T, val negated: Boolean) extends Selectable:
+sealed trait PropertyChecker[T, E]:
+  val failedMessage: String
+  def check(t: T, condition: Condition[E]): Boolean
+
+case class SingleChecker[T]() extends PropertyChecker[T, T]:
+  override def check(t: T, condition: Condition[T]): Boolean = condition.test(t)
+  override val failedMessage: String = "is not"
+
+case class NegatedChecker[T]() extends PropertyChecker[T, T]:
+  override def check(t: T, condition: Condition[T]): Boolean = !condition.test(t)
+  override val failedMessage: String = "is"
+
+case class AllChecker[E]() extends PropertyChecker[Iterable[E], E]:
+  override def check(t: Iterable[E], condition: Condition[E]): Boolean = t.forall(e => condition.test(e))
+  override val failedMessage: String = "has elements not satisfying"
+
+case class SomeChecker[E]() extends PropertyChecker[Iterable[E], E]:
+  override def check(t: Iterable[E], condition: Condition[E]): Boolean = t.exists(e => condition.test(e))
+  override val failedMessage: String = "has no elements satisfying"
+
+case class NoChecker[E]() extends PropertyChecker[Iterable[E], E]:
+  override def check(t: Iterable[E], condition: Condition[E]): Boolean = t.forall(e => !condition.test(e))
+  override val failedMessage: String = "has elements satisfying"
+
+class HavePropertyTypeProvider[T, E](val subject: T, val checker: PropertyChecker[T, E]) extends Selectable:
   def applyDynamic[U](fieldName: String)(arg: satisfying.type): SatisfyingNotEquals[U] = ???
   def applyDynamic(fieldName: String)(arg: Any): AssertionProperty = ???
 end HavePropertyTypeProvider
 
-sealed trait ContainsAssertionKind
-case object All extends ContainsAssertionKind
-case object None extends ContainsAssertionKind
-case object Some extends ContainsAssertionKind
-
-class ContainsPropertyTypeProvider[T](val subject: Iterable[T], val kind: ContainsAssertionKind) extends Selectable:
-  def applyDynamic[U](fieldName: String)(arg: satisfying.type): SatisfyingNotEquals[U] = ???
-  def applyDynamic(fieldName: String)(arg: Any): AssertionProperty = ???
-end ContainsPropertyTypeProvider
-
 /** A trait for each type of assertion (be or have).
   */
 sealed trait AssertionDSLVerb
@@ -60,10 +74,9 @@ case object be extends AssertionDSLVerb with Dynamic:
   def selectDynamic(fieldName: String): AssertionProperty = ???
 case object be_ extends AssertionDSLVerb
 
-sealed trait HaveVerb(val negated: Boolean):
-  inline def `unary_!`: HaveVerb = HaveNegation(this)
-case class HaveNegation(haveVerb: HaveVerb) extends HaveVerb(!haveVerb.negated)
-case object have extends HaveVerb(false)
+case object have extends AssertionDSLVerb:
+  inline def `unary_!`: have.type = ???
+
 
 case object contain extends AssertionDSLVerb
 case object `with` extends AssertionDSLVerb
@@ -72,15 +85,15 @@ case class ContainsVerb[T](subject: Iterable[T])
 
 extension [T](inline containsVerb: ContainsVerb[T])
   transparent inline def allElements(inline verb: `with`.type) = ${
-    ShouldContainTypeProvider.generateShouldContainTypeProvider('containsVerb, 'All)
+    ShouldContainTypeProvider.generateShouldContainTypeProvider('containsVerb, '{ AllChecker[T]() })
   }
 
   transparent inline def someElements(inline verb: `with`.type) = ${
-    ShouldContainTypeProvider.generateShouldContainTypeProvider('containsVerb, 'Some)
+    ShouldContainTypeProvider.generateShouldContainTypeProvider('containsVerb, '{ SomeChecker[T]() })
   }
 
   transparent inline def noElements(inline verb: `with`.type) = ${
-    ShouldContainTypeProvider.generateShouldContainTypeProvider('containsVerb, 'None)
+    ShouldContainTypeProvider.generateShouldContainTypeProvider('containsVerb, '{ NoChecker[T]() })
   }
 
 /** Implicit class to add 'should' assertions to a generic type T.
@@ -116,8 +129,8 @@ extension [T](inline subject: T)
     * @return
     *   a type provider for properties of type T.
     */
-  transparent inline def should(inline verb: HaveVerb) = ${
-    ShouldHaveTypeProvider.generateShouldHaveTypeProvider[T]('subject, '{verb.negated})
+  transparent inline def should(inline verb: have.type) = ${
+    ShouldHaveTypeProvider.generateShouldHaveTypeProvider[T]('subject, 'verb)
   }
 
   // We define here the 'should contain' extension method. It is not possible to
diff --git a/src/main/scala/ch/usi/si/msde/edsl/lecture10/Main.scala b/src/main/scala/ch/usi/si/msde/edsl/lecture10/Main.scala
index 9f23c4a..6b35fb2 100644
--- a/src/main/scala/ch/usi/si/msde/edsl/lecture10/Main.scala
+++ b/src/main/scala/ch/usi/si/msde/edsl/lecture10/Main.scala
@@ -46,7 +46,7 @@ case class Box(label: String, weight: Mass, price: Money)
     List() should have size satisfying >= 0
     List(3) should have size satisfying !== 0
     List(50, 2, 3) should have head satisfying < 100
-    box should !(!have) weight satisfying <= 300.0.kg
+    box should !have weight satisfying <= 300.0.kg
 
     // we wrap the strings in StringOps instances in order to resolve the scala method "size". This would otherwise
     // not happen automatically as the string types would resolve to "java.lang.String" thus not allowing the type
diff --git a/src/main/scala/ch/usi/si/msde/edsl/lecture10/ShouldContainTypeProvider.scala b/src/main/scala/ch/usi/si/msde/edsl/lecture10/ShouldContainTypeProvider.scala
index aefa73b..c2d77df 100644
--- a/src/main/scala/ch/usi/si/msde/edsl/lecture10/ShouldContainTypeProvider.scala
+++ b/src/main/scala/ch/usi/si/msde/edsl/lecture10/ShouldContainTypeProvider.scala
@@ -7,13 +7,10 @@ object ShouldContainTypeProvider:
   /** The type provider for the should have assertion, which generates a refined
     * structural type for type T.
     */
-  def generateShouldContainTypeProvider[T](containsExpr: Expr[ContainsVerb[T]], kind: Expr[ContainsAssertionKind])
+  def generateShouldContainTypeProvider[T](containsExpr: Expr[ContainsVerb[T]], checker: Expr[PropertyChecker[Iterable[T], T]])
                                           (using Type[T], Quotes): Expr[Any] =
     import quotes.reflect.*
 
-    println("containsExpr: " + containsExpr.show)
-    println("kind: " + kind.show)
-
     val subject: Expr[Iterable[T]] = containsExpr match
       case '{ ContainsVerb.apply[T]($s: Iterable[T]) } => s
 
@@ -77,11 +74,8 @@ object ShouldContainTypeProvider:
           Flags.Synthetic
         )
 
-    println("fields: " + fields)
-    println("arityZeroMethods: " + arityZeroMethods)
-
     val refinedType = refineTypeBySymbols(
-      TypeRepr.of[ContainsPropertyTypeProvider[T]],
+      TypeRepr.of[HavePropertyTypeProvider[Iterable[T], T]],
       fields ++ arityZeroMethods
     )
 
@@ -93,8 +87,6 @@ object ShouldContainTypeProvider:
     // exact type is unknown until compilation time.
     refinedType.asType match
       case '[tpe] => // tpe is the exact refined type
-        val a = '{ ContainsPropertyTypeProvider[T]($subject, $kind).asInstanceOf[tpe] }
-        println(a.show)
-        a
+        '{ HavePropertyTypeProvider[Iterable[T], T]($subject, $checker).asInstanceOf[tpe] }
 
 end ShouldContainTypeProvider
diff --git a/src/main/scala/ch/usi/si/msde/edsl/lecture10/ShouldHaveTypeProvider.scala b/src/main/scala/ch/usi/si/msde/edsl/lecture10/ShouldHaveTypeProvider.scala
index c678699..f068c0f 100644
--- a/src/main/scala/ch/usi/si/msde/edsl/lecture10/ShouldHaveTypeProvider.scala
+++ b/src/main/scala/ch/usi/si/msde/edsl/lecture10/ShouldHaveTypeProvider.scala
@@ -4,14 +4,23 @@ import scala.quoted.*
 
 object ShouldHaveTypeProvider:
 
+
+
   /** The type provider for the should have assertion, which generates a refined
     * structural type for type T.
     */
-  def generateShouldHaveTypeProvider[T](subject: Expr[T], negated: Expr[Boolean])(using Type[T])(using
+  def generateShouldHaveTypeProvider[T](subject: Expr[T], verb: Expr[have.type])(using Type[T])(using
       Quotes
   ): Expr[Any] =
     import quotes.reflect.*
 
+    def isNegated(verb: Expr[have.type]): Boolean =
+      verb match
+        case '{ ($inner: have.type).`unary_!` } => !isNegated(inner)
+        case '{ have: have.type } => false
+
+    val negated = isNegated(verb)
+
     // hack to get the equivalent of `TypeRepr.of[Function1[?, ?]]` (i.e. an arity-1 function type constructor).
     // Getting it as is returns an applied type with useless bounds (Nothing to Any), and the returned TypeRepr,
     // if re-applied to some `I` input type and `O` output type would be incompatible with `TypeRepr.of[I => O]` for
@@ -73,10 +82,12 @@ object ShouldHaveTypeProvider:
         )
 
     val refinedType = refineTypeBySymbols(
-      TypeRepr.of[HavePropertyTypeProvider[T]],
+      TypeRepr.of[HavePropertyTypeProvider[T, T]],
       fields ++ arityZeroMethods
     )
 
+    val checker = if (negated) '{ NegatedChecker[T]() } else '{ SingleChecker[T]() }
+
     // This is the way to extract a (reflection) type to a
     // type that can be used in some quoted code.
     // it's the equivalent of .asExpr for expressions,
@@ -84,6 +95,6 @@ object ShouldHaveTypeProvider:
     // exact type is unknown until compilation time.
     refinedType.asType match
       case '[tpe] => // tpe is the exact refined type
-        '{ HavePropertyTypeProvider[T]($subject, $negated).asInstanceOf[tpe] }
+        '{ HavePropertyTypeProvider[T, T]($subject, $checker).asInstanceOf[tpe] }
 
 end ShouldHaveTypeProvider