diff --git a/.scalafix.conf b/.scalafix.conf
index 43496f94..e94161b7 100644
--- a/.scalafix.conf
+++ b/.scalafix.conf
@@ -7,7 +7,7 @@ rules = [
   ProcedureSyntax
   RemoveUnused
   LeakingImplicitClassVal
-//  ExplicitResultTypes
+  ExplicitResultTypes
 ]
 
 RemoveUnused {
@@ -20,7 +20,7 @@ RemoveUnused {
 }
 
 ExplicitResultTypes {
-//  rewriteStructuralTypesToNamedSubclass = false
+  rewriteStructuralTypesToNamedSubclass = false
   skipSimpleDefinitions = false
 
   onlyImplicits = true
diff --git a/core/src/main/scala/shapesafe/core/arity/binary/Op2_Imp0.scala b/core/src/main/scala/shapesafe/core/arity/binary/Op2_Imp0.scala
index 4ae68f09..d71026c1 100644
--- a/core/src/main/scala/shapesafe/core/arity/binary/Op2_Imp0.scala
+++ b/core/src/main/scala/shapesafe/core/arity/binary/Op2_Imp0.scala
@@ -1,5 +1,6 @@
 package shapesafe.core.arity.binary
 
+import shapesafe.core.arity.ProveArity.|-
 import shapesafe.core.arity._
 
 trait Op2_Imp0 extends Op2Like_Imp0 {
@@ -11,7 +12,7 @@ trait Op2_Imp0 extends Op2Like_Imp0 {
   ](
       implicit
       domain: UncheckedDomain[A1, A2]
-  ) = {
+  ): OP#On[A1, A2] |- Unchecked = {
     domain.forOp2[OP]
   }
 }
diff --git a/prover-commons b/prover-commons
index fa2fd25f..2d098f7c 160000
--- a/prover-commons
+++ b/prover-commons
@@ -1 +1 @@
-Subproject commit fa2fd25fc06d090d0544221b2440f28bdbe797ad
+Subproject commit 2d098f7ced162bed53c16c102246ca6ce42b0af0