diff --git a/buildSrc b/buildSrc
index 6a5d144c..1f0d3457 160000
--- a/buildSrc
+++ b/buildSrc
@@ -1 +1 @@
-Subproject commit 6a5d144cfb9f0f638b9685467af97b6245f6b8f2
+Subproject commit 1f0d34578c08ab2f18e884a2c8e73aeed7a3bbc6
diff --git a/core/src/main/scala/shapesafe/core/SymbolicTuples.scala b/core/src/main/scala/shapesafe/core/SymbolicTuples.scala
new file mode 100644
index 00000000..f1393011
--- /dev/null
+++ b/core/src/main/scala/shapesafe/core/SymbolicTuples.scala
@@ -0,0 +1,43 @@
+package shapesafe.core
+
+import ai.acyclic.prover.commons.tuple.{ProductTuples, Tuples}
+import shapesafe.core.debugging.{HasNotation, Notations}
+import ai.acyclic.prover.commons.tuple.ProductTuples.EYE
+
+trait SymbolicTuples[VB] extends Tuples {
+
+  final type VBound = VB
+
+  object Backbone extends ProductTuples[VB]
+
+  trait Tuple extends Backbone.Tuple with HasNotation {
+
+//    final type Cons[HH <: VB] = BoneNotation.this.><[this.type, VB]
+    type _ConsExpr[PEEK <: HasNotation]
+  }
+
+  class Eye extends Backbone.Eye with Tuple {
+
+    final override type _ConsExpr[T <: HasNotation] = T#Notation
+    final override type Notation = EYE.T
+  }
+  override val Eye = new Eye
+
+  class ><[
+      TAIL <: Tuple,
+      HEAD <: VB
+  ](
+      tail: TAIL,
+      head: HEAD
+  ) extends Backbone.><[TAIL, HEAD](tail, head)
+      with Tuple {
+
+    type PeekHead <: HasNotation
+
+    final override type _ConsExpr[PEEK <: HasNotation] = Notations.><[this.Notation, PEEK#Notation]
+    final override type Notation = TAIL#_ConsExpr[PeekHead]
+  }
+
+  final override def cons[TAIL <: Tuple, HEAD <: VBound](tail: TAIL, head: HEAD): TAIL >< HEAD =
+    new ><(tail, head)
+}
diff --git a/core/src/main/scala/shapesafe/core/axis/Axis.scala b/core/src/main/scala/shapesafe/core/axis/Axis.scala
index 7c4c4bb7..bb9e596a 100644
--- a/core/src/main/scala/shapesafe/core/axis/Axis.scala
+++ b/core/src/main/scala/shapesafe/core/axis/Axis.scala
@@ -4,12 +4,12 @@ import ai.acyclic.prover.commons.same.Same
 import shapeless.Witness
 import shapeless.labelled.FieldType
 import shapesafe.core.arity.{Arity, ArityType, ConstArity}
-import shapesafe.core.debugging.{CanPeek, Notations}
+import shapesafe.core.debugging.{HasNotation, Notations}
 import shapesafe.core.{XInt, XString}
 
 import scala.language.implicitConversions
 
-trait Axis extends AxisLike with Same.ByEquality.IWrapper with CanPeek {
+trait Axis extends AxisLike with Same.ByEquality.IWrapper with HasNotation {
   // TODO:; can be a subclass of shapeless KeyTag
 
   final type Field = FieldType[Name, _ArityType]
@@ -42,12 +42,12 @@ object Axis {
 
     type _Axis = _ArityType :<<- Name
 
-    trait CanPeekName extends CanPeek {
+    trait NameAsNotation extends HasNotation {
 
       override type Notation = Name
     }
 
-    override type Notation = Notations.:<<-[A#Notation, CanPeekName#Notation]
+    override type Notation = Notations.:<<-[A#Notation, NameAsNotation#Notation]
 
     override lazy val toString: String = {
       if (name.isEmpty) s"$arityType"
diff --git a/core/src/main/scala/shapesafe/core/debugging/CanRefute.scala b/core/src/main/scala/shapesafe/core/debugging/CanRefute.scala
index 75d18c9a..244bb32a 100644
--- a/core/src/main/scala/shapesafe/core/debugging/CanRefute.scala
+++ b/core/src/main/scala/shapesafe/core/debugging/CanRefute.scala
@@ -1,6 +1,6 @@
 package shapesafe.core.debugging
 
-trait CanRefute extends CanPeek {
+trait CanRefute extends HasNotation {
 
   type _RefuteTxt
 
diff --git a/core/src/main/scala/shapesafe/core/debugging/ExpressionType.scala b/core/src/main/scala/shapesafe/core/debugging/ExpressionType.scala
index e071c49e..21ce34eb 100644
--- a/core/src/main/scala/shapesafe/core/debugging/ExpressionType.scala
+++ b/core/src/main/scala/shapesafe/core/debugging/ExpressionType.scala
@@ -3,7 +3,7 @@ package shapesafe.core.debugging
 import ai.acyclic.prover.commons.graph.local.Local
 import ai.acyclic.prover.commons.meta.ProductDiscovery
 
-trait ExpressionType extends CanPeek {}
+trait ExpressionType extends HasNotation {}
 
 object ExpressionType {
 
diff --git a/core/src/main/scala/shapesafe/core/debugging/CanPeek.scala b/core/src/main/scala/shapesafe/core/debugging/HasNotation.scala
similarity index 88%
rename from core/src/main/scala/shapesafe/core/debugging/CanPeek.scala
rename to core/src/main/scala/shapesafe/core/debugging/HasNotation.scala
index 9387516a..9a619091 100644
--- a/core/src/main/scala/shapesafe/core/debugging/CanPeek.scala
+++ b/core/src/main/scala/shapesafe/core/debugging/HasNotation.scala
@@ -1,6 +1,6 @@
 package shapesafe.core.debugging
 
-trait CanPeek {
+trait HasNotation {
 
   type Notation
   // use TypeVizCT macro
diff --git a/core/src/main/scala/shapesafe/core/debugging/NotationsLike.scala b/core/src/main/scala/shapesafe/core/debugging/NotationsLike.scala
index 202d523d..81a3f10f 100644
--- a/core/src/main/scala/shapesafe/core/debugging/NotationsLike.scala
+++ b/core/src/main/scala/shapesafe/core/debugging/NotationsLike.scala
@@ -43,13 +43,13 @@ object NotationsLike {
 
     trait On[A] {}
 
-    type Apply[AA <: CanPeek] = On[AA#Notation]
+    type Apply[AA <: HasNotation] = On[AA#Notation]
   }
   trait Proto2 {
 
     trait On[A, B] {}
 
-    type Apply[AA <: CanPeek, BB <: CanPeek] = On[AA#Notation, BB#Notation]
+    type Apply[AA <: HasNotation, BB <: HasNotation] = On[AA#Notation, BB#Notation]
   }
 
 }
diff --git a/core/src/main/scala/shapesafe/core/debugging/ProofWithReasoning.scala b/core/src/main/scala/shapesafe/core/debugging/ProofWithReasoning.scala
index 212ce7d6..0d431358 100644
--- a/core/src/main/scala/shapesafe/core/debugging/ProofWithReasoning.scala
+++ b/core/src/main/scala/shapesafe/core/debugging/ProofWithReasoning.scala
@@ -9,23 +9,23 @@ trait ProofWithReasoning extends ProofSystem with Reporters {
 
   trait Reasoner {
 
-    type Goal <: CanPeek
+    type Goal <: HasNotation
 
-    object Peek extends PeekReporter[CanPeek, Goal]
-    type Peek[I <: CanPeek] = Peek.CaseFrom[I]
+    object Peek extends PeekReporter[HasNotation, Goal]
+    type Peek[I <: HasNotation] = Peek.CaseFrom[I]
 
-    object Interrupt extends InterruptReporter[CanPeek, Goal]
-    type Interrupt[I <: CanPeek] = Interrupt.CaseFrom[I]
+    object Interrupt extends InterruptReporter[HasNotation, Goal]
+    type Interrupt[I <: HasNotation] = Interrupt.CaseFrom[I]
 
     trait ReasoningMixin {
       self: Proof[_, _] =>
     }
 
-    type |-@-[I <: CanPeek, O <: Goal] = (I |- O) with ReasoningMixin
+    type |-@-[I <: HasNotation, O <: Goal] = (I |- O) with ReasoningMixin
 
     object ReasoningMixin {
 
-      implicit def reason[I <: CanPeek, P <: Consequent](
+      implicit def reason[I <: HasNotation, P <: Consequent](
           implicit
           reporter: Peek.CaseFrom[I],
           prove: Proof[I, P]
diff --git a/core/src/main/scala/shapesafe/core/debugging/Reporters.scala b/core/src/main/scala/shapesafe/core/debugging/Reporters.scala
index d9465ee0..12b3cb47 100644
--- a/core/src/main/scala/shapesafe/core/debugging/Reporters.scala
+++ b/core/src/main/scala/shapesafe/core/debugging/Reporters.scala
@@ -13,16 +13,16 @@ trait Reporters extends HasTheory {
 
   import Reporters._
 
-  trait ProofReporter[IUB <: CanPeek, TGT <: CanPeek] extends Reporter {
+  trait ProofReporter[IUB <: HasNotation, TGT <: HasNotation] extends Reporter {
 
     import shapesafe.core.debugging.DebugConst._
     import theory._
 
-    type ExprOf[T <: CanPeek] = T#Notation
+    type ExprOf[T <: HasNotation] = T#Notation
 
     trait Step1_Imp3 extends AdHocPoly1 {
 
-      implicit def raw[A <: CanPeek, VA <: XString](
+      implicit def raw[A <: HasNotation, VA <: XString](
           implicit
           vizA: PeekCTAux[A#Notation, VA],
           mk: (CannotEval + VA + "\n") { type Out <: XString }
@@ -33,7 +33,7 @@ trait Reporters extends HasTheory {
     trait Step1_Imp2 extends Step1_Imp3 {
 
       implicit def eval[
-          A <: CanPeek,
+          A <: HasNotation,
           S <: TGT,
           VA <: XString,
           VS <: XString
@@ -50,7 +50,7 @@ trait Reporters extends HasTheory {
     trait Step1_Imp1 extends Step1_Imp2 {
 
       implicit def alreadyEvaled[
-          S <: TGT with CanPeek,
+          S <: TGT with HasNotation,
           VS <: XString
       ](
           implicit
@@ -63,12 +63,12 @@ trait Reporters extends HasTheory {
     override object Step1 extends Step1_Imp1
   }
 
-  trait PeekReporter[IUB <: CanPeek, TGT <: CanPeek] extends ProofReporter[IUB, TGT] {
+  trait PeekReporter[IUB <: HasNotation, TGT <: HasNotation] extends ProofReporter[IUB, TGT] {
 
     override type EmitMsg[T] = Emit.Info[T]
   }
 
-  trait InterruptReporter[IUB <: CanPeek, TGT <: CanPeek] extends ProofReporter[IUB, TGT] {
+  trait InterruptReporter[IUB <: HasNotation, TGT <: HasNotation] extends ProofReporter[IUB, TGT] {
 
     override type EmitMsg[T] = Emit.Error[T]
   }
diff --git a/core/src/main/scala/shapesafe/core/package.scala b/core/src/main/scala/shapesafe/core/package.scala
index 5ee9e754..961cae19 100644
--- a/core/src/main/scala/shapesafe/core/package.scala
+++ b/core/src/main/scala/shapesafe/core/package.scala
@@ -1,7 +1,11 @@
 package shapesafe
 
+import ai.acyclic.prover.commons.function.PreDef
+
 package object core {
 
   type XInt = Int with Singleton
   type XString = String with Singleton
+
+  type AdHocPoly1 = PreDef.Poly
 }
diff --git a/core/src/main/scala/shapesafe/core/shape/Dimensions.scala b/core/src/main/scala/shapesafe/core/shape/Dimensions.scala
index a8cdac0b..2556b1e0 100644
--- a/core/src/main/scala/shapesafe/core/shape/Dimensions.scala
+++ b/core/src/main/scala/shapesafe/core/shape/Dimensions.scala
@@ -1,7 +1,8 @@
 package shapesafe.core.shape
 
+import ai.acyclic.prover.commons.tuple.ProductTuples
+import shapesafe.core.SymbolicTuples
 import shapesafe.core.arity.ArityType
-import shapesafe.core.tuple.Bone
 
 // should it be "Arities"?
-object Dimensions extends Bone[ArityType] {}
+object Dimensions extends SymbolicTuples[ArityType] {}
diff --git a/core/src/main/scala/shapesafe/core/shape/Index.scala b/core/src/main/scala/shapesafe/core/shape/Index.scala
index a17d052a..0e2e11e7 100644
--- a/core/src/main/scala/shapesafe/core/shape/Index.scala
+++ b/core/src/main/scala/shapesafe/core/shape/Index.scala
@@ -1,11 +1,11 @@
 package shapesafe.core.shape
 
 import shapesafe.core.arity.Utils.NatAsOp
-import shapesafe.core.debugging.CanPeek
+import shapesafe.core.debugging.HasNotation
 import ai.acyclic.prover.commons.same.Same
 import shapeless.{Nat, Witness}
 
-trait Index extends Same.ByEquality.IWrapper with CanPeek {
+trait Index extends Same.ByEquality.IWrapper with HasNotation {
 
   def value: Any
   final override protected def samenessDelegatedTo = value
diff --git a/core/src/main/scala/shapesafe/core/shape/Indices.scala b/core/src/main/scala/shapesafe/core/shape/Indices.scala
index 32db8dba..941fed3c 100644
--- a/core/src/main/scala/shapesafe/core/shape/Indices.scala
+++ b/core/src/main/scala/shapesafe/core/shape/Indices.scala
@@ -1,6 +1,7 @@
 package shapesafe.core.shape
 
-import shapesafe.core.tuple.{Bone, Tuples}
+import ai.acyclic.prover.commons.tuple.Tuples
+import shapesafe.core.SymbolicTuples
 
 trait Indices extends IndicesMagnet with Indices.Backbone.Tuple {
 
@@ -13,7 +14,7 @@ object Indices extends Tuples {
 
   type VBound = Index
 
-  object Backbone extends Bone[VBound] {}
+  object Backbone extends SymbolicTuples[VBound] {}
 
   type Tuple = Indices
 
diff --git a/core/src/main/scala/shapesafe/core/shape/Names.scala b/core/src/main/scala/shapesafe/core/shape/Names.scala
index 82d0a672..edd44704 100644
--- a/core/src/main/scala/shapesafe/core/shape/Names.scala
+++ b/core/src/main/scala/shapesafe/core/shape/Names.scala
@@ -1,24 +1,24 @@
 package shapesafe.core.shape
 
-import shapesafe.core.XString
-import shapesafe.core.debugging.CanPeek
-import shapesafe.core.shape.args.ApplyLiterals
-import shapesafe.core.tuple._
+import ai.acyclic.prover.commons.tuple._
 import shapeless.Witness
+import shapesafe.core.debugging.HasNotation
+import shapesafe.core.shape.args.ApplyLiterals
+import shapesafe.core.{SymbolicTuples, XString}
 
 import scala.language.implicitConversions
 
-trait Names extends IndicesMagnet with Names.Proto.Tuple {}
+trait Names extends IndicesMagnet with Names.Backbone.Tuple {}
 
 object Names extends Tuples with ApplyLiterals.ToNames {
 
   type VBound = XString // expand to take all String for gradual typing?
 
-  object Proto extends Bone[VBound] {}
+  object Backbone extends SymbolicTuples[VBound] {}
 
   type Tuple = Names
 
-  class Eye extends Proto.Eye with Names {
+  class Eye extends Backbone.Eye with Names {
     override type AsIndices = Indices.Eye
 
     override def asIndices: Indices.Eye = Indices.Eye
@@ -31,17 +31,19 @@ object Names extends Tuples with ApplyLiterals.ToNames {
   ](
       override val tail: TAIL,
       override val head: HEAD
-  ) extends Proto.><[TAIL, HEAD](tail, head)
+  ) extends Backbone.><[TAIL, HEAD](tail, head)
       with Tuple {
 
     val headW: Witness.Aux[HEAD] = Witness[HEAD](head).asInstanceOf[Witness.Aux[HEAD]]
 
     override type AsIndices = Indices.><[tail.AsIndices, Index.Name[HEAD]]
 
-    override def asIndices: AsIndices =
+    override def asIndices: AsIndices = {
+      import Indices._
       tail.asIndices >< Index.Name(headW)
+    }
 
-    trait PeekHead extends CanPeek {
+    trait PeekHead extends HasNotation {
       override type Notation = Head
     }
   }
diff --git a/core/src/main/scala/shapesafe/core/shape/StaticShape.scala b/core/src/main/scala/shapesafe/core/shape/StaticShape.scala
index 0c0df244..01543acb 100644
--- a/core/src/main/scala/shapesafe/core/shape/StaticShape.scala
+++ b/core/src/main/scala/shapesafe/core/shape/StaticShape.scala
@@ -1,13 +1,13 @@
 package shapesafe.core.shape
 
+import ai.acyclic.prover.commons.tuple.Tuples
 import shapeless.{::, HList, HNil, Nat, Succ, Witness}
+import shapesafe.core.Const.NoName
 import shapesafe.core.arity.Utils.NatAsOp
 import shapesafe.core.arity.{Arity, ArityType, ConstArity}
 import shapesafe.core.axis.Axis
 import shapesafe.core.axis.Axis.{->>, :<<-}
-import shapesafe.core.Const.NoName
-import shapesafe.core.tuple.{Bone, Tuples}
-import shapesafe.core.{XInt, XString}
+import shapesafe.core.{SymbolicTuples, XInt, XString}
 
 /**
   * a thin wrapper of HList that has all proofs of constraints included this saves compiler burden and reduces error
@@ -32,7 +32,7 @@ object StaticShape extends Tuples {
 
   final type VBound = Axis
 
-  object Backbone extends Bone[VBound]
+  object Backbone extends SymbolicTuples[VBound]
   type Proto = Backbone.Tuple
 
   final type Tuple = StaticShape
diff --git a/core/src/main/scala/shapesafe/core/shape/VerifiedShape.scala b/core/src/main/scala/shapesafe/core/shape/VerifiedShape.scala
deleted file mode 100644
index 326b19f3..00000000
--- a/core/src/main/scala/shapesafe/core/shape/VerifiedShape.scala
+++ /dev/null
@@ -1,17 +0,0 @@
-//package shapesafe.core.shape
-//
-//import ProveShape._
-//
-//trait VerifiedShape extends Shape {}
-//
-//object VerifiedShape { // TODO: remove, none of the shape can be verified unless their underlying arities are
-//
-//  implicit def endo[T <: VerifiedShape]: T =>> T = ProveShape.forAll[T].=>>(identity[T])
-//
-//  //  abstract class ProvenAs[O <: LeafArity]()(
-//  //      implicit
-//  //      val out: O
-//  //  ) extends Proven
-//  //      with ProveArity.Of[O] {}
-//
-//}
diff --git a/core/src/main/scala/shapesafe/core/tuple/Bone.scala b/core/src/main/scala/shapesafe/core/tuple/Bone.scala
deleted file mode 100644
index 797992f1..00000000
--- a/core/src/main/scala/shapesafe/core/tuple/Bone.scala
+++ /dev/null
@@ -1,91 +0,0 @@
-package shapesafe.core.tuple
-
-import shapesafe.core.debugging.{CanPeek, Notations}
-import shapesafe.core.util.HListView
-import ai.acyclic.prover.commons.same.Same
-import ai.acyclic.prover.commons.typesetting.TextBlock
-import shapeless.{::, HList, HNil, Witness}
-
-trait Bone[VB] extends Tuples {
-
-  import Bone._
-
-  final type VBound = VB
-
-  trait Tuple extends Same.ByEquality.IWrapper with CanPeek {
-
-    type Static <: HList
-    def static: Static
-    lazy val staticView: HListView[Static] = HListView(static)
-
-    def asList: List[VB]
-
-    override protected def samenessDelegatedTo: Any = asList
-
-    final type Cons[HH <: VB] = Bone.this.><[this.type, VB]
-    type _ConsExpr[PEEK <: CanPeek]
-  }
-
-  class Eye extends Tuple {
-
-    override type Static = HNil
-    override def static: HNil = HNil
-
-    override def asList: List[VB] = Nil
-
-    override lazy val toString: String = EYE.value
-
-    final override type _ConsExpr[T <: CanPeek] = T#Notation
-    final override type Notation = EYE.T
-  }
-  override val Eye = new Eye
-
-  // cartesian product symbol
-  class ><[
-      TAIL <: Tuple,
-      HEAD <: VB
-  ](
-      val tail: TAIL,
-      val head: HEAD
-  ) extends Tuple {
-
-    // in scala 3 these will be gone
-    type Tail = TAIL
-    type Head = HEAD
-
-    override type Static = HEAD :: tail.Static
-    override def static: Static = head :: tail.static
-
-    override def asList: List[VB] = tail.asList ++ Seq(head)
-
-    override lazy val toString: String = {
-      val tailStr = tail match {
-        case _: Eye => ""
-        case _      => tail.toString + " ><\n"
-      }
-
-      s"""$tailStr${TextBlock(head.toString).indent("  ").build}
-         | """.stripMargin.trim
-    }
-
-    type PeekHead <: CanPeek
-
-    final override type _ConsExpr[PEEK <: CanPeek] = Notations.><[this.Notation, PEEK#Notation]
-    final override type Notation = TAIL#_ConsExpr[PeekHead]
-  }
-
-  final override def cons[TAIL <: Tuple, HEAD <: VBound](tail: TAIL, head: HEAD): TAIL >< HEAD =
-    new ><(tail, head)
-}
-
-object Bone {
-
-  val EYE = Witness("∅")
-
-  object W {
-
-    final val eye = Witness("Eye")
-
-    final val >< = Witness(" >< ")
-  }
-}
diff --git a/core/src/main/scala/shapesafe/core/tuple/CanInfix.scala b/core/src/main/scala/shapesafe/core/tuple/CanInfix.scala
deleted file mode 100644
index 0fd6d21f..00000000
--- a/core/src/main/scala/shapesafe/core/tuple/CanInfix.scala
+++ /dev/null
@@ -1,7 +0,0 @@
-//package shapesafe.core.tuple
-//
-//import scala.language.implicitConversions
-//
-//trait CanInfix extends CanCons {}
-//
-//object CanInfix {}
diff --git a/core/src/main/scala/shapesafe/core/tuple/TupleSystem.scala b/core/src/main/scala/shapesafe/core/tuple/TupleSystem.scala
deleted file mode 100644
index e9b83bb3..00000000
--- a/core/src/main/scala/shapesafe/core/tuple/TupleSystem.scala
+++ /dev/null
@@ -1,30 +0,0 @@
-package shapesafe.core.tuple
-
-import shapesafe.core.AdHocPoly1
-import shapeless.HNil
-
-trait TupleSystem {
-
-  type VBound
-
-  type Tuple
-
-  type Eye <: Tuple
-  val Eye: Eye
-//  final type Eye = Eye.type
-
-  trait HListIntake extends AdHocPoly1 {
-
-    final val outer = TupleSystem.this
-
-    implicit val toEye: HNil =>> Eye = {
-      at[HNil].defining { _ =>
-        Eye
-      }
-    }
-  }
-
-  object HListIntake {}
-}
-
-object TupleSystem {}
diff --git a/core/src/main/scala/shapesafe/core/tuple/Tuples.scala b/core/src/main/scala/shapesafe/core/tuple/Tuples.scala
deleted file mode 100644
index 598af932..00000000
--- a/core/src/main/scala/shapesafe/core/tuple/Tuples.scala
+++ /dev/null
@@ -1,56 +0,0 @@
-package shapesafe.core.tuple
-
-import shapeless.{::, HList}
-
-import scala.language.implicitConversions
-
-trait Tuples extends TupleSystem {
-
-  type ><[TAIL <: Tuple, HEAD <: VBound] <: Tuple
-
-  def cons[TAIL <: Tuple, HEAD <: VBound](tail: TAIL, head: HEAD): TAIL >< HEAD
-
-  trait ConsIntake[B <: VBound] extends HListIntake {
-
-    implicit def inductive[
-        H_TAIL <: HList,
-        TAIL <: Tuple,
-        HEAD <: B
-    ](
-        implicit
-        forTail: H_TAIL =>> TAIL
-    ): (HEAD :: H_TAIL) =>> ><[TAIL, HEAD] = {
-
-      at[HEAD :: H_TAIL].defining { v =>
-        val prev = apply(v.tail)
-
-        cons(prev, v.head)
-      }
-    }
-  }
-
-  object FromStatic extends ConsIntake[VBound] {}
-
-  object FromLiterals extends ConsIntake[VBound with Singleton] {}
-
-  trait InfixMixin[SELF <: Tuple] {
-
-    def self: SELF
-
-    def ><[
-        HEAD <: VBound
-    ](
-        head: HEAD
-    ): SELF >< HEAD = cons(self, head)
-
-    def &[
-        HEAD <: VBound
-    ](
-        head: HEAD
-    ): SELF >< HEAD = cons(self, head)
-  }
-
-  implicit class tupleExtension[SELF <: Tuple](val self: SELF) extends InfixMixin[SELF] {}
-
-  implicit def eyeExtension(s: this.type): tupleExtension[Eye] = tupleExtension[Eye](Eye)
-}
diff --git a/core/src/main/scala/shapesafe/core/util/HListView.scala b/core/src/main/scala/shapesafe/core/util/HListView.scala
deleted file mode 100644
index ccb630f7..00000000
--- a/core/src/main/scala/shapesafe/core/util/HListView.scala
+++ /dev/null
@@ -1,34 +0,0 @@
-package shapesafe.core.util
-
-import shapeless.labelled.FieldType
-import shapeless.ops.record.Selector
-import shapeless.{HList, Poly1}
-
-case class HListView[H <: HList](hh: H) {
-
-  // https://stackoverflow.com/questions/66036106/can-shapeless-record-type-be-used-as-a-poly1-part-2
-  trait GetV extends Poly1 {
-
-    implicit def getter[S](
-        implicit
-        _selector: Selector[H, S]
-    ): Case.Aux[S, _selector.Out] = at[S] { _ =>
-      _selector(hh)
-    }
-  }
-  object GetV extends GetV
-
-  trait GetField extends Poly1 {
-
-    implicit def getter[S](
-        implicit
-        _selector: Selector[H, S]
-    ): Case.Aux[S, FieldType[S, _selector.Out]] = at[S] { _ =>
-      _selector(hh).asInstanceOf[FieldType[S, _selector.Out]]
-    }
-  }
-  object GetField extends GetField
-
-}
-
-object HListView {}
diff --git a/core/src/test/scala/shapesafe/core/util/HListViewSpec.scala b/core/src/test/scala/shapesafe/core/util/HListViewSpec.scala
index f4f7a215..53965651 100644
--- a/core/src/test/scala/shapesafe/core/util/HListViewSpec.scala
+++ b/core/src/test/scala/shapesafe/core/util/HListViewSpec.scala
@@ -1,5 +1,6 @@
 package shapesafe.core.util;
 
+import ai.acyclic.prover.commons.tuple.HListView
 import shapesafe.BaseSpec
 import shapeless.HNil;
 
diff --git a/prover-commons b/prover-commons
index 39f62305..cebcf1f3 160000
--- a/prover-commons
+++ b/prover-commons
@@ -1 +1 @@
-Subproject commit 39f62305335019b2f015140c689c407eb325342d
+Subproject commit cebcf1f3fd735ade06bb162a3ac5be912a3abd2c
diff --git a/splain b/splain
index 023383b2..79c28c7a 160000
--- a/splain
+++ b/splain
@@ -1 +1 @@
-Subproject commit 023383b23d982655549bf259b184eb741dadab0a
+Subproject commit 79c28c7a16b6f71bf9eca83a9ead759f1adbedb4