diff --git a/core/src/main/scala/shapesafe/core/AdHocPoly1.scala b/core/src/main/scala/shapesafe/core/AdHocPoly1.scala
deleted file mode 100644
index 368cc354..00000000
--- a/core/src/main/scala/shapesafe/core/AdHocPoly1.scala
+++ /dev/null
@@ -1,10 +0,0 @@
-package shapesafe.core
-
-import ai.acyclic.prover.commons.function.PreDef
-
-/**
-  * Different from dotty's polymorphic function kind, which only supports parametric polymorphic
-  */
-trait AdHocPoly1 extends PreDef.Poly {}
-
-object AdHocPoly1 {}
diff --git a/core/src/main/scala/shapesafe/core/Const.scala b/core/src/main/scala/shapesafe/core/Const.scala
index 3d8bad74..9015492a 100644
--- a/core/src/main/scala/shapesafe/core/Const.scala
+++ b/core/src/main/scala/shapesafe/core/Const.scala
@@ -1,11 +1,9 @@
 package shapesafe.core
 
-import shapeless.Witness
-
 object Const {
 
   type NoName = ""
-  lazy val NoNameW: Witness.Aux[NoName] = Witness[NoName]
+  lazy val NoNameW: "" = ""
 
   object True // TODO: should already exists in scala library
   type True = True.type
diff --git a/core/src/main/scala/shapesafe/core/SymbolicTuples.scala b/core/src/main/scala/shapesafe/core/SymbolicTuples.scala
index f1393011..f1650442 100644
--- a/core/src/main/scala/shapesafe/core/SymbolicTuples.scala
+++ b/core/src/main/scala/shapesafe/core/SymbolicTuples.scala
@@ -19,7 +19,7 @@ trait SymbolicTuples[VB] extends Tuples {
   class Eye extends Backbone.Eye with Tuple {
 
     final override type _ConsExpr[T <: HasNotation] = T#Notation
-    final override type Notation = EYE.T
+    final override type Notation = EYE.type
   }
   override val Eye = new Eye
 
diff --git a/core/src/main/scala/shapesafe/core/arity/Arity.scala b/core/src/main/scala/shapesafe/core/arity/Arity.scala
index 9f22b618..29cb719d 100644
--- a/core/src/main/scala/shapesafe/core/arity/Arity.scala
+++ b/core/src/main/scala/shapesafe/core/arity/Arity.scala
@@ -1,12 +1,13 @@
 package shapesafe.core.arity
 
-import shapeless.{Nat, Witness}
+import ai.acyclic.prover.commons.refl.XInt
+import shapeless.Nat
 import shapesafe.core.arity.ConstArity.{Derived, Literal}
 import shapesafe.core.arity.Utils.NatAsOp
 import shapesafe.core.arity.ops.ArityOpsLike
 import shapesafe.core.axis.Axis
 import shapesafe.core.debugging.CanReason
-import shapesafe.core.{arity, Const, XInt}
+import shapesafe.core.{arity, Const}
 
 import scala.language.implicitConversions
 
@@ -57,7 +58,7 @@ trait Arity extends CanReason with ArityOpsLike with Axis {
       prove: ReasonTo[O]
   ): ^[O] = eval(prove)
 
-  final override val nameW: Witness.Aux[Const.NoName] = Const.NoNameW
+  final override val nameW: Const.NoName = Const.NoNameW
 }
 
 object Arity {
@@ -80,8 +81,8 @@ object Arity {
 
   val Unchecked: ^[arity.Unchecked.type] = arity.Unchecked.^
 
-  def apply(w: Witness.Lt[XInt]): ^[Literal[w.T]] = {
-    ^(Literal.shapeless(w))
+  def apply[S <: XInt](w: S): ^[Literal[S]] = {
+    ^(Literal(w))
   }
 
   object FromNat {
diff --git a/core/src/main/scala/shapesafe/core/arity/ConstArity.scala b/core/src/main/scala/shapesafe/core/arity/ConstArity.scala
index bb734dcf..136073e1 100644
--- a/core/src/main/scala/shapesafe/core/arity/ConstArity.scala
+++ b/core/src/main/scala/shapesafe/core/arity/ConstArity.scala
@@ -1,8 +1,7 @@
 package shapesafe.core.arity
 
+import ai.acyclic.prover.commons.refl.XInt
 import ai.acyclic.prover.commons.same.Same
-import shapeless.Witness
-import shapesafe.core.XInt
 import shapesafe.core.arity.Utils.Op
 import singleton.ops.{==, Require}
 
@@ -20,20 +19,18 @@ trait ConstArity[S] extends LeafArity with Same.ByEquality.IWrapper {
       proof: S =:= N2
   ): Unit = {}
 
-  def proveEqualType[N2](
+  def proveEqualType[N2 <: XInt](
       implicit
       proof: Require[S == N2]
   ): Unit = {}
 
   // TODO: should be named proofEqual, require should do everything in runtime?
-  def proveEqual(w: Witness.Lt[Int])(
+  def proveEqual[N2 <: XInt](n2: N2)(
       implicit
-      proof: Require[S == w.T]
+      proof: Require[S == N2]
   ): Unit = {
 
-    proveEqualType[w.T]
-
-    require(w.value == runtimeValue)
+    require(n2 == runtimeValue)
   }
 }
 
@@ -63,14 +60,10 @@ object ConstArity {
 
     implicit def summon[S <: XInt](
         implicit
-        w: Witness.Aux[S]
+        w: ValueOf[S]
     ): Literal[S] = {
       new Literal[S](w.value)
     }
 
-    def shapeless(w: Witness.Lt[XInt]): Literal[w.T] = {
-
-      Literal.summon[w.T](w)
-    }
   }
 }
diff --git a/core/src/main/scala/shapesafe/core/arity/binary/Op2.scala b/core/src/main/scala/shapesafe/core/arity/binary/Op2.scala
index 961d756b..a4b67a16 100644
--- a/core/src/main/scala/shapesafe/core/arity/binary/Op2.scala
+++ b/core/src/main/scala/shapesafe/core/arity/binary/Op2.scala
@@ -38,7 +38,7 @@ object Op2 extends Op2_Imp0 {
       // TODO: can this be VerifiedArity?
 
       override type _RefuteTxt =
-        DebugConst.REFUTE.T + DebugConst.ILLEGAL_OP.T + A1#SymbolTxt + SS[
+        DebugConst.REFUTE.type + DebugConst.ILLEGAL_OP.type + A1#SymbolTxt + SS[
           Unit,
           Unit
         ]#SymbolTxt + A2#SymbolTxt
diff --git a/core/src/main/scala/shapesafe/core/arity/binary/Require2.scala b/core/src/main/scala/shapesafe/core/arity/binary/Require2.scala
index c639c184..4e8f3474 100644
--- a/core/src/main/scala/shapesafe/core/arity/binary/Require2.scala
+++ b/core/src/main/scala/shapesafe/core/arity/binary/Require2.scala
@@ -43,7 +43,7 @@ object Require2 extends Require2_Imp0 {
     ) extends Conjecture2[A1, A2] {
 
       override type _RefuteTxt =
-        DebugConst.REFUTE.T + A1#SymbolTxt + SS[Unit, Unit]#Negation#SymbolTxt + A2#SymbolTxt
+        DebugConst.REFUTE.type + A1#SymbolTxt + SS[Unit, Unit]#Negation#SymbolTxt + A2#SymbolTxt
 
       override lazy val runtimeValue: Int = {
         val v1 = a1.runtimeValue
diff --git a/core/src/main/scala/shapesafe/core/axis/Axis.scala b/core/src/main/scala/shapesafe/core/axis/Axis.scala
index bb9e596a..c5270742 100644
--- a/core/src/main/scala/shapesafe/core/axis/Axis.scala
+++ b/core/src/main/scala/shapesafe/core/axis/Axis.scala
@@ -1,11 +1,10 @@
 package shapesafe.core.axis
 
+import ai.acyclic.prover.commons.refl.{XInt, XString}
 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.{HasNotation, Notations}
-import shapesafe.core.{XInt, XString}
 
 import scala.language.implicitConversions
 
@@ -32,7 +31,7 @@ object Axis {
       N <: XString
   ](
       val arityType: A,
-      val nameW: Witness.Aux[N]
+      val nameW: N
   ) extends Axis
       //      with KeyTag[N, D :<<- N]
       // TODO: remove? FieldType[] has some black magic written in macro
@@ -40,7 +39,7 @@ object Axis {
 
     type _ArityType = A
 
-    type _Axis = _ArityType :<<- Name
+    type _Axis = _ArityType :<<- N
 
     trait NameAsNotation extends HasNotation {
 
@@ -55,19 +54,16 @@ object Axis {
     }
   }
 
-  def apply(
+  def apply[N <: XString](
       value: Arity,
-      name: Witness.Lt[XString]
-  ): :<<-[value._ArityType, name.T] = {
+      name: N
+  ): :<<-[value._ArityType, N] = {
 
     new :<<-(value.arityType, name)
   }
 
-  implicit def fromXInt[V <: XInt](v: V)(
-      implicit
-      toW: Witness.Aux[V]
-  ): Arity.^[ConstArity.Literal[V]] = {
+  implicit def fromXInt[V <: XInt](v: V): Arity.^[ConstArity.Literal[V]] = {
 
-    Arity(toW)
+    Arity(v)
   }
 }
diff --git a/core/src/main/scala/shapesafe/core/axis/AxisLike.scala b/core/src/main/scala/shapesafe/core/axis/AxisLike.scala
index cc05e559..30deeb89 100644
--- a/core/src/main/scala/shapesafe/core/axis/AxisLike.scala
+++ b/core/src/main/scala/shapesafe/core/axis/AxisLike.scala
@@ -1,29 +1,28 @@
 package shapesafe.core.axis
 
-import shapesafe.core.XString
+import ai.acyclic.prover.commons.refl.XString
 import shapesafe.core.arity.Arity
 import shapesafe.core.arity.ops.HasArity
 import shapesafe.core.axis.Axis.:<<-
-import shapeless.Witness
 
 trait AxisLike extends HasArity {
 
-  val nameW: Witness.Lt[XString]
-  final type Name = nameW.T
+  val nameW: XString
+  final type Name = nameW.type
 
-  final def name: Name = nameW.value
+  final def name: Name = nameW
 
   def nameless: Arity.^[_ArityType] = arityType.^
 
   def namedT[S <: XString](
       implicit
-      name: Witness.Aux[S]
+      name: S
   ): _ArityType :<<- S = Axis(nameless, name)
 
-  def named(name: Witness.Lt[XString]): _ArityType :<<- name.T = {
+  def named[S <: XString](name: S): _ArityType :<<- S = {
 
     namedT(name)
   }
 
-  def :<<-(name: Witness.Lt[XString]): _ArityType :<<- name.T = namedT(name)
+  def :<<-[S <: XString](name: S): _ArityType :<<- S = namedT(name)
 }
diff --git a/core/src/main/scala/shapesafe/core/axis/OldNameUpdaters.scala b/core/src/main/scala/shapesafe/core/axis/OldNameUpdaters.scala
index e393e6f2..6965d02d 100644
--- a/core/src/main/scala/shapesafe/core/axis/OldNameUpdaters.scala
+++ b/core/src/main/scala/shapesafe/core/axis/OldNameUpdaters.scala
@@ -1,10 +1,11 @@
 package shapesafe.core.axis
 
+import ai.acyclic.prover.commons.refl.XString
 import shapesafe.core.arity.binary.Op2Like
 import shapesafe.core.arity.{ArityType, LeafArity}
 import shapesafe.core.axis.Axis.->>
 import shapeless.ops.record.{Modifier, Selector}
-import shapeless.{::, HList, Witness}
+import shapeless.{::, HList}
 
 class OldNameUpdaters[OP <: Op2Like](val op: OP) {
 
@@ -16,13 +17,13 @@ class OldNameUpdaters[OP <: Op2Like](val op: OP) {
 
     implicit def ifOldName[
         OLD <: HList,
-        N <: String,
+        N <: XString,
         A1 <: ArityType,
         A2 <: ArityType,
         O <: LeafArity
     ](
         implicit
-        name: Witness.Aux[N],
+        name: ValueOf[N],
         selector: Selector.Aux[OLD, N, A1],
         lemma: op.On[A1, A2] |- O
     ): (OLD, N ->> A2) =>> ((N ->> O) :: OLD) = {
@@ -32,7 +33,7 @@ class OldNameUpdaters[OP <: Op2Like](val op: OP) {
         case (old, field) =>
           import shapeless.record._
 
-          val d1 = old.apply(name)
+          val d1 = selector.apply(old)
           val d2 = field: A2
 
           val oped = op.on(d1.^, d2.^)
@@ -52,13 +53,13 @@ class OldNameUpdaters[OP <: Op2Like](val op: OP) {
 
     implicit def ifOldName[
         OLD <: HList,
-        N <: String,
+        N <: XString,
         A1 <: ArityType,
         A2 <: ArityType,
         O <: LeafArity
     ](
         implicit
-        name: Witness.Aux[N],
+        name: N,
         selector: Selector.Aux[OLD, N, A1], // TODO: how to remove this? should be implied in modifier
         lemma: op.On[A1, A2] |- O,
         modifier: Modifier[OLD, N, A1, O]
diff --git a/core/src/main/scala/shapesafe/core/debugging/DebugConst.scala b/core/src/main/scala/shapesafe/core/debugging/DebugConst.scala
index bfd63c41..6ee9cb9b 100644
--- a/core/src/main/scala/shapesafe/core/debugging/DebugConst.scala
+++ b/core/src/main/scala/shapesafe/core/debugging/DebugConst.scala
@@ -1,6 +1,5 @@
 package shapesafe.core.debugging
 
-import shapeless.Witness
 import singleton.ops.{+, ITE, IsString}
 
 object DebugConst {
@@ -19,37 +18,37 @@ object DebugConst {
   //    TypeToLiteral.Type.Case[T1]
   //  ]
 
-  val SPACE4 = Witness("    ")
-  val shades_+ = Witness(" ░▒▓")
-  val shades_- = Witness("▓▒░ ")
+  final val SPACE4 = "    "
+  final val shades_+ = " ░▒▓"
+  final val shades_- = "▓▒░ "
 
-  type Stripe[T] = SPACE4.T + shades_-.T + T + shades_+.T + "\n\n"
+  type Stripe[T] = SPACE4.type + shades_-.type + T + shades_+.type + "\n\n"
 
   // TODO: add another instance that shows reasoning process?
 
-//  val LF = Witness("\n")
+//  val LF = ("\n")
 
-  val EMPTY = Witness("")
+  val EMPTY = ""
 
-  val REFUTE =
-    Witness("""¯\_(ツ)_/¯ """)
-  val PEEK =
-    Witness("""      """)
-  val EQUIV =
-    Witness("""  :=  """)
+  final val REFUTE =
+    """¯\_(ツ)_/¯ """
+  final val PEEK =
+    """      """
+  final val EQUIV =
+    """  :=  """
 
-  type EquivLF = "\n" + EQUIV.T
+  type EquivLF = "\n" + EQUIV.type
 
   type CannotEval = Stripe["cannot evaluate"]
 
-  val ILLEGAL_OP = Witness("""(Illegal Operation) """)
+  final val ILLEGAL_OP = """(Illegal Operation) """
 
-  val IMPOSSIBLE = Witness("IMPOSSIBLE!")
+  final val IMPOSSIBLE = "IMPOSSIBLE!"
 
   type Br[T] = "(" + T + ")"
 
-  val FROM1 = Witness("\n\n... with 1 prior >\n\n")
-  val FROM2 = Witness("\n\n... with 2 priors >\n\n")
+  final val FROM1 = "\n\n... with 1 prior >\n\n"
+  final val FROM2 = "\n\n... with 2 priors >\n\n"
 
   val INTERNAL_ERROR = "[INTERNAL ERROR] Please submit a bug report using the following expression ..."
 }
diff --git a/core/src/main/scala/shapesafe/core/debugging/Reporters.scala b/core/src/main/scala/shapesafe/core/debugging/Reporters.scala
index 12b3cb47..2ee5b567 100644
--- a/core/src/main/scala/shapesafe/core/debugging/Reporters.scala
+++ b/core/src/main/scala/shapesafe/core/debugging/Reporters.scala
@@ -42,7 +42,7 @@ trait Reporters extends HasTheory {
           lemma: A |- S,
           vizA: PeekCTAux[A#Notation, VA],
           vizS: PeekCTAux[ExprOf[S], VS],
-          mk: (PEEK.T + VS + EquivLF + VA + "\n") { type Out <: XString }
+          mk: (PEEK.type + VS + EquivLF + VA + "\n") { type Out <: XString }
       ): A =>> mk.Out =
         at[A].defining(_ => mk.value)
     }
@@ -55,7 +55,7 @@ trait Reporters extends HasTheory {
       ](
           implicit
           vizS: PeekCTAux[ExprOf[S], VS],
-          op: (PEEK.T + VS + "\n") { type Out <: XString }
+          op: (PEEK.type + VS + "\n") { type Out <: XString }
       ): S =>> op.Out =
         at[S].defining(_ => op.value)
     }
diff --git a/core/src/main/scala/shapesafe/core/logic/binary/RingAxioms.scala b/core/src/main/scala/shapesafe/core/logic/binary/RingAxioms.scala
index 462b29c6..17dab226 100644
--- a/core/src/main/scala/shapesafe/core/logic/binary/RingAxioms.scala
+++ b/core/src/main/scala/shapesafe/core/logic/binary/RingAxioms.scala
@@ -14,7 +14,7 @@ trait RingAxioms[D, :+[A <: D, B <: D] <: D, :*[A <: D, B <: D] <: D, _0 <: D, _
         A <: D,
         B <: D,
         C <: D
-    ] = forAll[A :* (B :+ C)].=>> { v =>
+    ]: theory.Theorem[A :* (B :+ C) |- (A :* B :+ (A :* C))] = forAll[A :* (B :+ C)].=>> { v =>
       val (l, r) = deconstruct(v)
       val (rl, rr) = group_+.deconstruct(r)
 
@@ -28,7 +28,7 @@ trait RingAxioms[D, :+[A <: D, B <: D] <: D, :*[A <: D, B <: D] <: D, _0 <: D, _
         A <: D,
         B <: D,
         C <: D
-    ] = forAll[(A :+ B) :* C].=>> { v =>
+    ]: theory.Theorem[A :+ B :* C |- (A :* C :+ (B :* C))] = forAll[(A :+ B) :* C].=>> { v =>
       val (l, r) = deconstruct(v)
       val (ll, lr) = group_+.deconstruct(l)
 
diff --git a/core/src/main/scala/shapesafe/core/package.scala b/core/src/main/scala/shapesafe/core/package.scala
index 961cae19..fed5a6a0 100644
--- a/core/src/main/scala/shapesafe/core/package.scala
+++ b/core/src/main/scala/shapesafe/core/package.scala
@@ -4,8 +4,5 @@ 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/Index.scala b/core/src/main/scala/shapesafe/core/shape/Index.scala
index 0e2e11e7..aba12e5b 100644
--- a/core/src/main/scala/shapesafe/core/shape/Index.scala
+++ b/core/src/main/scala/shapesafe/core/shape/Index.scala
@@ -1,9 +1,10 @@
 package shapesafe.core.shape
 
+import ai.acyclic.prover.commons.refl.XString
 import shapesafe.core.arity.Utils.NatAsOp
 import shapesafe.core.debugging.HasNotation
 import ai.acyclic.prover.commons.same.Same
-import shapeless.{Nat, Witness}
+import shapeless.Nat
 
 trait Index extends Same.ByEquality.IWrapper with HasNotation {
 
@@ -18,18 +19,17 @@ object Index {
   trait Name_<:[+KUB] extends Index {}
   type Str = Name_<:[String]
 
-  class Name[S <: String](val w: Witness.Aux[S]) extends Name_<:[S] {
-    def name: S = w.value
+  class Name[S <: XString](val name: S) extends Name_<:[S] {
     type Name = S
 
-    override def value = w.value
+    override def value = name
 
     override type Notation = S
   }
 
   object Name {
 
-    def apply(w: Witness.Lt[String]): Name[w.T] = new Name(w)
+    def apply[S <: XString](w: S): Name[S] = new Name(w)
   }
 
   class LtoR[N <: Nat, S <: Int](val index: N, override val value: S) extends Name_<:[Nothing] {
diff --git a/core/src/main/scala/shapesafe/core/shape/Names.scala b/core/src/main/scala/shapesafe/core/shape/Names.scala
index edd44704..6ccc0c70 100644
--- a/core/src/main/scala/shapesafe/core/shape/Names.scala
+++ b/core/src/main/scala/shapesafe/core/shape/Names.scala
@@ -1,10 +1,10 @@
 package shapesafe.core.shape
 
+import ai.acyclic.prover.commons.refl.XString
 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 shapesafe.core.SymbolicTuples
 
 import scala.language.implicitConversions
 
@@ -34,7 +34,7 @@ object Names extends Tuples with ApplyLiterals.ToNames {
   ) extends Backbone.><[TAIL, HEAD](tail, head)
       with Tuple {
 
-    val headW: Witness.Aux[HEAD] = Witness[HEAD](head).asInstanceOf[Witness.Aux[HEAD]]
+    val headW: HEAD = head
 
     override type AsIndices = Indices.><[tail.AsIndices, Index.Name[HEAD]]
 
@@ -56,20 +56,14 @@ object Names extends Tuples with ApplyLiterals.ToNames {
 
   trait Syntax {
 
-    implicit def literalToNames(v: String)(
-        implicit
-        w: Witness.Aux[v.type]
-    ): Eye >< v.type = {
+    implicit def literalToNames[V <: XString](v: V): Eye >< v.type = {
 
-      Eye >< w.value
+      Eye >< v
     }
 
-    implicit def literalToExtension(v: String)(
-        implicit
-        w: Witness.Aux[v.type]
-    ): tupleExtension[Eye >< v.type] = {
+    implicit def literalToExtension[V <: XString](v: V): tupleExtension[Eye >< v.type] = {
 
-      tupleExtension(Eye >< w.value)
+      tupleExtension(Eye >< v)
     }
   }
 
diff --git a/core/src/main/scala/shapesafe/core/shape/Shape.scala b/core/src/main/scala/shapesafe/core/shape/Shape.scala
index ec30bf71..560ac456 100644
--- a/core/src/main/scala/shapesafe/core/shape/Shape.scala
+++ b/core/src/main/scala/shapesafe/core/shape/Shape.scala
@@ -1,7 +1,10 @@
 package shapesafe.core.shape
 
+import ai.acyclic.prover.commons.refl.{XInt, XString}
 import shapeless.ops.hlist.Reverse
-import shapeless.{HList, Nat, SingletonProductArgs, Witness}
+import shapeless.{HList, Nat, SingletonProductArgs}
+import shapesafe.core.Const.True
+import shapesafe.core.Ops
 import shapesafe.core.arity.Utils.NatAsOp
 import shapesafe.core.arity.{Arity, ConstArity}
 import shapesafe.core.axis.Axis
@@ -11,7 +14,6 @@ import shapesafe.core.shape.args.{ApplyLiterals, ApplyNats}
 import shapesafe.core.shape.binary.OuterProduct
 import shapesafe.core.shape.ops.{EinSumOp, MatrixOps, StaticOpsView, VectorOps}
 import shapesafe.core.shape.unary._
-import shapesafe.core.{Ops, XInt}
 
 import scala.language.implicitConversions
 
@@ -23,8 +25,8 @@ trait Shape extends CanReason with VectorOps with MatrixOps {
 
   override def expressionType = shapeType
 
+  import shapesafe.core.shape.ProveShape.AsLeafShape._
   import theory._
-  import AsLeafShape._
 
   final override def toString: String = shapeType.toString
 
@@ -134,9 +136,13 @@ trait Shape extends CanReason with VectorOps with MatrixOps {
       apply(Index.LtoR(i))
     }
 
-    def apply(w: Witness.Lt[String]): ^[Select1[_ShapeType, Index.Name[w.T]]] = {
+    def apply[S <: XString](s: S)(
+        implicit
+        ev: True
+    ): ^[Select1[_ShapeType, Index.Name[S]]] = {
 
-      apply(Index.Name(w))
+      val name: Index.Name[S] = Index.Name(s)
+      apply(name)
     }
   }
 
@@ -206,12 +212,10 @@ object Shape extends Shape with ApplyLiterals.ToShape {
 
   implicit def unbox[S <: ShapeType](v: Aux[S]): S = v.shapeType
 
-  implicit def fromXInt[T <: XInt](v: T)(
-      implicit
-      toW: Witness.Aux[T]
-  ): ^[StaticShape.Eye ><^ ConstArity.Literal[T]] = {
+  implicit def fromXInt[T <: XInt](v: T): ^[StaticShape.Eye ><^ ConstArity.Literal[T]] = {
 
-    ^(Shape and Arity(toW))
+    val and: StaticShape.Eye ><^ ConstArity.Literal[T] = Shape and Arity[T](v)
+    ^(and)
   }
 
   implicit def asStatic[T <: StaticShape](v: Aux[T]): StaticOpsView[T] = StaticOpsView(v.shapeType)
diff --git a/core/src/main/scala/shapesafe/core/shape/StaticShape.scala b/core/src/main/scala/shapesafe/core/shape/StaticShape.scala
index 01543acb..636aa888 100644
--- a/core/src/main/scala/shapesafe/core/shape/StaticShape.scala
+++ b/core/src/main/scala/shapesafe/core/shape/StaticShape.scala
@@ -1,13 +1,14 @@
 package shapesafe.core.shape
 
+import ai.acyclic.prover.commons.refl.{XInt, XString}
 import ai.acyclic.prover.commons.tuple.Tuples
-import shapeless.{::, HList, HNil, Nat, Succ, Witness}
+import shapeless.{::, HList, HNil, Nat, Succ}
 import shapesafe.core.Const.NoName
+import shapesafe.core.SymbolicTuples
 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.{SymbolicTuples, XInt, XString}
 
 /**
   * a thin wrapper of HList that has all proofs of constraints included this saves compiler burden and reduces error
@@ -71,7 +72,7 @@ object StaticShape extends Tuples {
     final override type NatNumOfDimensions = Succ[tail.NatNumOfDimensions]
 
     final override type _Names = Names.><[tail._Names, head.Name]
-    final override val names = new Names.><(tail.names, head.nameW.value)
+    final override val names = new Names.><(tail.names, head.nameW)
 
     final override type _Dimensions = Dimensions.><[tail._Dimensions, head._ArityType]
     final override val dimensions = new Dimensions.><(tail.dimensions, head.arityType)
@@ -120,7 +121,7 @@ object StaticShape extends Tuples {
     ](
         implicit
         forTail: H_TAIL =>> TAIL,
-        w: Witness.Aux[N]
+        w: N
     ): ((N ->> C) :: H_TAIL) =>> (TAIL >< (C :<<- N)) = {
 
       at[(N ->> C) :: H_TAIL].defining { v =>
@@ -166,13 +167,12 @@ object StaticShape extends Tuples {
         HEAD <: XInt
     ](
         implicit
-        forTail: H_TAIL =>> TAIL,
-        w: Witness.Aux[HEAD]
+        forTail: H_TAIL =>> TAIL
     ): (HEAD :: H_TAIL) =>> (TAIL ><^ ConstArity.Literal[HEAD]) = {
 
       at[HEAD :: H_TAIL].defining { v =>
         val prev = forTail(v.tail)
-        val head = Arity(w) // Arity.Impl(ConstArity.Literal(w))
+        val head = Arity[HEAD](v.head) // Arity.Impl(ConstArity.Literal(w))
 
         prev.^ _and head
       }
diff --git a/core/src/main/scala/shapesafe/core/shape/unary/Select1.scala b/core/src/main/scala/shapesafe/core/shape/unary/Select1.scala
index 15fa4fb8..d812fbb5 100644
--- a/core/src/main/scala/shapesafe/core/shape/unary/Select1.scala
+++ b/core/src/main/scala/shapesafe/core/shape/unary/Select1.scala
@@ -1,15 +1,16 @@
 package shapesafe.core.shape.unary
 
+import ai.acyclic.prover.commons.refl.XString
 import shapeless.ops.hlist.{At, Reverse}
 import shapeless.ops.record.Selector
-import shapeless.{HList, Nat, Witness}
+import shapeless.{HList, Nat}
+import shapesafe.core.AdHocPoly1
 import shapesafe.core.arity.ArityType
 import shapesafe.core.axis.Axis
 import shapesafe.core.axis.Axis.:<<-
 import shapesafe.core.debugging.Notations
 import shapesafe.core.shape.StaticShape.><
 import shapesafe.core.shape._
-import shapesafe.core.{AdHocPoly1, XString}
 
 case class Select1[
     S1 <: ShapeType,
@@ -61,7 +62,7 @@ object Select1 extends Select1_Imp0 {
         val p1: P1 = v.s1
 
         val arity: A = _selector(p1.record)
-        val w: Witness.Aux[N] = v.index.w
+        val w: N = v.index.name
         arity.^ :<<- w
       }
     }
diff --git a/core/src/test/scala/shapesafe/core/arity/LeafAritySpec.scala b/core/src/test/scala/shapesafe/core/arity/LeafAritySpec.scala
index 53163a63..60bcfd23 100644
--- a/core/src/test/scala/shapesafe/core/arity/LeafAritySpec.scala
+++ b/core/src/test/scala/shapesafe/core/arity/LeafAritySpec.scala
@@ -1,31 +1,31 @@
 package shapesafe.core.arity
 
+import ai.acyclic.prover.commons.refl.XInt
 import shapesafe.BaseSpec
 import shapesafe.core.arity.ConstArity.{Derived, Literal}
 import shapesafe.m.PeerType
-import shapeless.Witness.Lt
 import singleton.ops.{+, ==, Require, ToInt}
 
 class LeafAritySpec extends BaseSpec {
 
   describe("big") {
 
-    def validate[S](subject: ConstArity[S], w: Lt[Int])(
+    def validate[S, S2 <: XInt](subject: ConstArity[S], w: S2)(
         implicit
-        proof: Require[S == w.T],
-        plus: S + w.T
+        proof: Require[S == S2],
+        plus: S + S2
     ): Unit = {
 
       val out = subject
       val out2 = subject
 
-      subject.proveEqual(w)(proof)
-      out.proveEqual(w)(proof) // scala compiler may fumble on this one
-      out2.proveEqual(w)(proof)
+      subject.proveEqual[S2](w)(proof)
+      out.proveEqual[S2](w)(proof) // scala compiler may fumble on this one
+      out2.proveEqual[S2](w)(proof)
 
-      implicitly[subject.SS + w.T]
-      implicitly[out.SS + w.T]
-      implicitly[out2.SS + w.T]
+      implicitly[subject.SS + S2]
+      implicitly[out.SS + S2]
+      implicitly[out2.SS + S2]
     }
 
     it("FromOp") {
@@ -39,7 +39,7 @@ class LeafAritySpec extends BaseSpec {
       }
 
       {
-        val v = Derived.summon[ToInt[big.w.T]]
+        val v = Derived.summon[ToInt[big.w.type]]
         validate(v, 100)
       }
     }
@@ -52,9 +52,10 @@ class LeafAritySpec extends BaseSpec {
       }
 
       {
-        val v = implicitly[Literal[big.w.T]]
+        val v = implicitly[Literal[big.w.type]]
         validate(v, 100)
       }
+
     }
   }
 
diff --git a/core/src/test/scala/shapesafe/core/arity/nullary/SizeOfSpec.scala b/core/src/test/scala/shapesafe/core/arity/nullary/SizeOfSpec.scala
index 341453ca..bd3f2fc9 100644
--- a/core/src/test/scala/shapesafe/core/arity/nullary/SizeOfSpec.scala
+++ b/core/src/test/scala/shapesafe/core/arity/nullary/SizeOfSpec.scala
@@ -22,7 +22,7 @@ class SizeOfSpec extends ArityFixture {
 
     it("big") {
 
-      implicitly[Require[big.nat.N == big.w.T]] // just a sanity check
+      implicitly[Require[big.nat.N == big.w.type]] // just a sanity check
 
       val op1 = SizeOf.getConst(big.hList).^
       op1.proveEqual(100)
diff --git a/core/src/test/scala/shapesafe/core/shape/NamesSpec.scala b/core/src/test/scala/shapesafe/core/shape/NamesSpec.scala
index 2933eec7..ebefad51 100644
--- a/core/src/test/scala/shapesafe/core/shape/NamesSpec.scala
+++ b/core/src/test/scala/shapesafe/core/shape/NamesSpec.scala
@@ -3,7 +3,7 @@ package shapesafe.core.shape
 import shapesafe.BaseSpec
 import shapesafe.core.shape.Index.Name
 import shapesafe.core.shape.Indices.tupleExtension
-import shapeless.{HNil, Witness}
+import shapeless.HNil
 
 class NamesSpec extends BaseSpec {
 
@@ -54,8 +54,8 @@ class NamesSpec extends BaseSpec {
 //      """implicitly[Names.Cons[Names.Eye, String]]"""
 //    )
 
-    val w = Witness("a")
-    val hh = Names.Eye >< w.value
+    val w = "a"
+    val hh = Names.Eye >< w
 
     hh.toString
       .shouldBe(
diff --git a/core/src/test/scala/shapesafe/core/shape/SingletonConstraintSpike.scala b/core/src/test/scala/shapesafe/core/shape/SingletonConstraintSpike.scala
index 366de9e8..3b937474 100644
--- a/core/src/test/scala/shapesafe/core/shape/SingletonConstraintSpike.scala
+++ b/core/src/test/scala/shapesafe/core/shape/SingletonConstraintSpike.scala
@@ -2,7 +2,7 @@ package shapesafe.core.shape
 
 import ai.acyclic.prover.commons.testlib.BaseSpec
 import org.scalatest.Ignore
-import shapeless.Witness
+
 
 @Ignore
 class SingletonConstraintSpike extends BaseSpec {
diff --git a/core/src/testFixtures/scala/shapesafe/BaseSpec.scala b/core/src/testFixtures/scala/shapesafe/BaseSpec.scala
index d7b059d9..96e126aa 100644
--- a/core/src/testFixtures/scala/shapesafe/BaseSpec.scala
+++ b/core/src/testFixtures/scala/shapesafe/BaseSpec.scala
@@ -1,10 +1,11 @@
 package shapesafe
 
-import ai.acyclic.prover.commons.testlib
 import ai.acyclic.prover.commons.meta.ScalaReflection
+import ai.acyclic.prover.commons.refl.XInt
+import ai.acyclic.prover.commons.testlib
 import ai.acyclic.prover.commons.viz.TypeViz
+import shapeless.{HList, Nat}
 import shapesafe.m.viz.PeekCT
-import shapeless.{HList, Nat, Witness}
 
 trait BaseSpec extends testlib.BaseSpec with TypeViz.TestFixtures {
 
@@ -39,9 +40,9 @@ object BaseSpec {
 
     val hList: HList
 
-    val w: Witness { type T <: Int }
+    val w: XInt
 
-    final def number = w.value
+    final def number = w
   }
 
   object small extends TypeN {
@@ -50,7 +51,7 @@ object BaseSpec {
 
     val hList = HList.fill[Double](nat)(0.0)
 
-    val w = Witness(6)
+    final val w = 6
   }
 
   /**
@@ -72,7 +73,7 @@ object BaseSpec {
 
     val hList = HList.fill[Double](nat)(0.0)
 
-    val w = Witness(100)
+    final val w = 100
 //    type W = w.T
   }
 }
diff --git a/gradle.properties b/gradle.properties
index 60760e99..3d1f72d3 100644
--- a/gradle.properties
+++ b/gradle.properties
@@ -7,7 +7,7 @@ scalaVersion=2.13.13
 #noVerify
 noSpike
 
-#splainVersion=1.1.0-SNAPSHOT
+splainVersion=1.1.0-SNAPSHOT
 
 org.gradle.caching=true // too many false assumptions, plus project is small at the moment
 org.gradle.parallel=true
\ No newline at end of file
diff --git a/macro2/src/main/scala/shapesafe/m/Emit.scala b/macro2/src/main/scala/shapesafe/m/Emit.scala
index 0f7d1181..dbe0a1ef 100644
--- a/macro2/src/main/scala/shapesafe/m/Emit.scala
+++ b/macro2/src/main/scala/shapesafe/m/Emit.scala
@@ -1,13 +1,12 @@
 package shapesafe.m
 
-import shapeless.Witness
 import singleton.ops.RequireMsg
 
 object Emit {
 
-  val FALSE = Witness(false)
+  val FALSE: false = false
 
-  type Error[T] = RequireMsg[FALSE.T, T]
+  type Error[T] = RequireMsg[FALSE.type, T]
 //  type Error[T] = RequireMsg[FALSE.T, "\n" + T]
 //  type Error[T] = GenericMsgEmitter[T, GenericMsgEmitter.Abort]
 
diff --git a/macro2/src/test/scala/shapesafe/m/viz/KindVizCTSpec.scala b/macro2/src/test/scala/shapesafe/m/viz/KindVizCTSpec.scala
index ea2015bf..1bf5ef7e 100644
--- a/macro2/src/test/scala/shapesafe/m/viz/KindVizCTSpec.scala
+++ b/macro2/src/test/scala/shapesafe/m/viz/KindVizCTSpec.scala
@@ -2,7 +2,7 @@ package shapesafe.m.viz
 
 import ai.acyclic.prover.commons.viz.format.FormatOvrd.{~~, SingletonName}
 import shapesafe.m.GenericMsgEmitter
-import shapeless.Witness
+
 import singleton.ops.+
 
 class KindVizCTSpec extends VizCTSpec {
@@ -42,7 +42,7 @@ class KindVizCTSpec extends VizCTSpec {
 
   describe(kindNoTree.toString) {
 
-    val groundTruth = TypeVizShort.infer["Int"](Witness("Int").value)
+    val groundTruth = TypeVizShort.infer["Int"]("Int")
 
     it("ground truth") {
 
diff --git a/prover-commons b/prover-commons
index cebcf1f3..4eeeb3b2 160000
--- a/prover-commons
+++ b/prover-commons
@@ -1 +1 @@
-Subproject commit cebcf1f3fd735ade06bb162a3ac5be912a3abd2c
+Subproject commit 4eeeb3b29031a0243f907ec2bc1db9364ad02824
diff --git a/verify/breeze/src/main/scala/shapesafe/verify/breeze/tensor/DoubleVector.scala b/verify/breeze/src/main/scala/shapesafe/verify/breeze/tensor/DoubleVector.scala
index d11cc47b..67bf06b0 100644
--- a/verify/breeze/src/main/scala/shapesafe/verify/breeze/tensor/DoubleVector.scala
+++ b/verify/breeze/src/main/scala/shapesafe/verify/breeze/tensor/DoubleVector.scala
@@ -1,9 +1,9 @@
 package shapesafe.verify.breeze.tensor
 
+import ai.acyclic.prover.commons.refl.XInt
 import breeze.linalg.DenseVector
 import breeze.signal
-import shapeless.{HList, ProductArgs, Witness}
-import shapesafe.core.XInt
+import shapeless.{HList, ProductArgs}
 import shapesafe.core.arity.ConstArity.Literal
 import shapesafe.core.arity.ProveArity.{|-, |-<}
 import shapesafe.core.arity.nullary.SizeOf
@@ -56,9 +56,9 @@ class DoubleVector[A1 <: ArityType](
     new DoubleVector(v.^, data)
   }
 
-  def pad[O <: LeafArity](padding: Witness.Lt[XInt])(
+  def pad[O <: LeafArity, S <: XInt](padding: S)(
       implicit
-      lemma: (A1 :+ (Literal[padding.T] :* Arity._2._ArityType)) |- O
+      lemma: (A1 :+ (Literal[S] :* Arity._2._ArityType)) |- O
   ): DoubleVector[O] = {
 
     val _padding = Arity(padding)
@@ -75,13 +75,14 @@ class DoubleVector[A1 <: ArityType](
 
   def conv[
       A2 <: ArityType,
-      O <: LeafArity
+      O <: LeafArity,
+      S <: XInt
   ](
       kernel: DoubleVector[A2],
-      stride: Witness.Lt[XInt]
+      stride: S
   )(
       implicit
-      lemma: ((A1 :- A2 :+ Arity._1._ArityType) :/ Literal[stride.T]) |- O
+      lemma: ((A1 :- A2 :+ Arity._1._ArityType) :/ Literal[S]) |- O
   ): DoubleVector[O] = {
 
     val _stride = Arity(stride)
@@ -90,7 +91,7 @@ class DoubleVector[A1 <: ArityType](
     val v = lemma.instanceFor(op)
     val out = v.^
 
-    val range = 0.to(this.data.size - kernel.data.size, stride.value)
+    val range = 0.to(this.data.size - kernel.data.size, stride)
 
 //    for (padding = 0.to(that.data.size - this.data.size))
     val dOut: DenseVector[Double] = signal.convolve(
@@ -144,13 +145,13 @@ object DoubleVector extends ProductArgs {
     }
   }
 
-  def zeros(lit: Witness.Lt[XInt]): DoubleVector[Literal[lit.T]] = {
+  def zeros[S <: XInt](lit: S): DoubleVector[Literal[S]] = {
 
-    new DoubleVector(Arity(lit), DenseVector.fill(lit.value)(0.0))
+    new DoubleVector(Arity(lit), DenseVector.fill(lit)(0.0))
   }
 
-  def random(lit: Witness.Lt[XInt]): DoubleVector[Literal[lit.T]] = {
-    val list = DenseVector.fill(lit.value) {
+  def random[S <: XInt](lit: S): DoubleVector[Literal[S]] = {
+    val list = DenseVector.fill(lit) {
       Random.nextDouble()
     }