diff --git a/base/Nat/AddExp.kind b/base/Nat/AddExp.kind
new file mode 100644
index 00000000..091ae9db
--- /dev/null
+++ b/base/Nat/AddExp.kind
@@ -0,0 +1,155 @@
+type Nat.AddExp {
+  const(value: Nat)
+  var(idx: Nat)
+  add(left: Nat.AddExp, right: Nat.AddExp)
+}
+
+Nat.AddExp.from_nat: Nat -> Nat.AddExp
+  Nat.AddExp.const
+
+Nat.AddExp.dimension(
+  exp: Nat.AddExp
+): Nat
+  case exp {
+    const:
+      0
+    add:
+      let left_dim = Nat.AddExp.dimension(exp.left)
+      let right_dim = Nat.AddExp.dimension(exp.right)
+      Nat.max(left_dim, right_dim)
+    var:
+      Nat.succ(exp.idx)
+  }
+
+Nat.AddExp.constant(exp: Nat.AddExp): Type
+  case exp {
+    const:
+      Unit
+    var:
+      Empty
+    add:
+      And<Nat.AddExp.constant(exp.left), Nat.AddExp.constant(exp.right)>
+  }
+
+Nat.AddExp.dimension.zero(
+  exp: Nat.AddExp
+  Hyp: Equal<Nat>(Nat.AddExp.dimension(exp), 0)
+): Nat.AddExp.constant(exp)
+  (case exp {
+    const:
+      (Hyp)
+        unit
+    var:
+      (Hyp)
+        let contra = Nat.succ_neq_zero!(Hyp)
+        Empty.absurd!(contra)
+    add:
+      (Hyp)
+        let {left_small, right_small} = Nat.max.big(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
+        def max = Nat.max(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
+        let left_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
+          max, 0, Hyp,
+          (x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.left), x), true),
+          left_small
+        ))
+        let right_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
+          max, 0, Hyp
+          (x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.right), x), true),
+          right_small
+        ))
+        let left = Nat.AddExp.dimension.zero(exp.left, left_zero)
+        let right = Nat.AddExp.dimension.zero(exp.right, right_zero)
+        Pair.new!!(left, right)
+  }: (Hyp: Equal<Nat>(Nat.AddExp.dimension(exp), 0)) -> Nat.AddExp.constant(exp))(
+    Hyp
+  )
+
+Nat.AddExp.compute(
+  exp: Nat.AddExp
+  Hyp: Nat.AddExp.constant(exp)
+): Nat
+  case exp with Hyp {
+    const:
+      exp.value
+    var:
+      Empty.absurd!(Hyp)
+    add:
+      open Hyp
+      Nat.add(Nat.AddExp.compute(exp.left, Hyp.fst), Nat.AddExp.compute(exp.right, Hyp.snd))
+  }!
+
+Nat.AddExp.substitution(
+  exp: Nat.AddExp
+): Variadic(Nat.AddExp.dimension(exp), Nat, Nat)
+  def dim = Nat.AddExp.dimension(exp)
+  def Hyp = Nat.Order.refl(dim)
+  Nat.AddExp.substitution.aux0(dim, exp, Hyp)
+
+Nat.AddExp.substitution.aux0(
+  n: Nat
+  exp: Nat.AddExp
+  Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), n), true)
+): Variadic(n, Nat, Nat)
+  case n with Hyp {
+    zero:
+      def Hyp = Nat.Order.chain.aux!(Hyp)
+      def Hyp = Nat.AddExp.dimension.zero!(Hyp)
+      Nat.AddExp.compute(exp, Hyp)
+    succ:
+      (value)
+        def new_exp = Nat.AddExp.substitution.aux1(exp, value, n.pred)
+        let Hyp = Nat.AddExp.substitution.aux2(exp, value, n.pred, Hyp)
+        Nat.AddExp.substitution.aux0(n.pred, new_exp, Hyp)
+  }!
+
+Nat.AddExp.substitution.aux1(
+  exp: Nat.AddExp
+  value: Nat
+  idx: Nat
+): Nat.AddExp
+  case exp {
+    const:
+      exp
+    var:
+      case Nat.lte(idx, exp.idx) {
+        true:
+          Nat.AddExp.const(value)
+        false:
+          exp
+      }
+    add:
+      Nat.AddExp.add(
+        Nat.AddExp.substitution.aux1(exp.left, value, idx)
+        Nat.AddExp.substitution.aux1(exp.right, value, idx)
+      )
+  }
+
+Nat.AddExp.substitution.aux2(
+  exp: Nat.AddExp
+  value: Nat
+  idx: Nat
+  Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), Nat.succ(idx)), true)
+): let new_exp = Nat.AddExp.substitution.aux1(exp, value, idx)
+   Equal<Bool>(Nat.lte(Nat.AddExp.dimension(new_exp), idx), true)
+  case exp with Hyp {
+    const:
+      Equal.refl<Bool>(true)
+    var:
+      def cmp = Nat.lte(idx, exp.idx)
+      let cmp_eq = refl :: cmp == cmp
+      case cmp with cmp_eq: ^cmp == cmp {
+        true:
+          Equal.refl<Bool>(true)
+        false:
+          Nat.lte.comm.false(idx, exp.idx, cmp_eq)
+      }! :: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(cmp(() Nat.AddExp, Nat.AddExp.const(value), Nat.AddExp.var(exp.idx))), idx), true)
+    add:
+      let {left_bound, right_bound} = Nat.max.split.left(
+        Nat.AddExp.dimension(exp.left),
+        Nat.AddExp.dimension(exp.right),
+        Nat.succ(idx), Hyp
+      )
+      let ind_left = Nat.AddExp.substitution.aux2(exp.left, value, idx, left_bound)
+      let ind_right = Nat.AddExp.substitution.aux2(exp.right, value, idx, right_bound)
+      Nat.max.combine.left!!!(ind_left, ind_right)
+  }!
diff --git a/base/Nat/lte/comm.kind b/base/Nat/lte/comm.kind
index b023a88b..c0d428c9 100644
--- a/base/Nat/lte/comm.kind
+++ b/base/Nat/lte/comm.kind
@@ -2,12 +2,12 @@ Nat.lte.comm.false(
   a: Nat
   b: Nat
   Hyp: Equal<Bool>(Nat.lte(a, b), false)
-): Equal<Bool>(Nat.lte(b, a), true)
+): Equal<Bool>(Nat.lte(Nat.succ(b), a), true)
   (case a {
     zero:
       (Hyp)
         let contra = Bool.true_neq_false(Hyp)
-        Empty.absurd<Equal<Bool>(Nat.lte(b, 0), true)>(contra)
+        Empty.absurd<Equal<Bool>(Nat.lte(Nat.succ(b), 0), true)>(contra)
     succ:
       (Hyp)
         (case b {
@@ -18,10 +18,10 @@ Nat.lte.comm.false(
             (Hyp)
               let qed = Nat.lte.comm.false(a.pred, b.pred, Hyp)
               qed
-        }: (Hyp: Equal<Bool>(Nat.lte(Nat.succ(a.pred), b), false)) -> Equal<Bool>(Nat.lte(b, Nat.succ(a.pred)), true))(
+        }: (Hyp: Equal<Bool>(Nat.lte(Nat.succ(a.pred), b), false)) -> Equal<Bool>(Nat.lte(Nat.succ(b), Nat.succ(a.pred)), true))(
           Hyp
         )
-  }: (Hyp: Equal<Bool>(Nat.lte(a, b), false)) -> Equal<Bool>(Nat.lte(b, a), true))(
+  }: (Hyp: Equal<Bool>(Nat.lte(a, b), false)) -> Equal<Bool>(Nat.lte(Nat.succ(b), a), true))(
     Hyp
   )
 
diff --git a/base/Nat/lte/succ_left.kind b/base/Nat/lte/succ_left.kind
new file mode 100644
index 00000000..58e28317
--- /dev/null
+++ b/base/Nat/lte/succ_left.kind
@@ -0,0 +1,17 @@
+Nat.lte.succ_left(
+  a: Nat
+  b: Nat
+  Hyp: Equal<Bool>(Nat.lte(Nat.succ(a), b), true)
+): Equal<Bool>(Nat.lte(a, b), true)
+  case b with Hyp {
+    zero:
+      let contra = Bool.false_neq_true(Hyp)
+      Empty.absurd!(contra)
+    succ:
+      case a with Hyp {
+        zero:
+          refl
+        succ:
+          Nat.lte.succ_left(a.pred, b.pred, Hyp)
+      }!
+  }!
diff --git a/base/Nat/max/big.kind b/base/Nat/max/big.kind
index 35eaab1a..d97aae23 100644
--- a/base/Nat/max/big.kind
+++ b/base/Nat/max/big.kind
@@ -11,6 +11,7 @@ Nat.max.big(
     false:
       (lemma_ab)
         let lemma_ba = Nat.lte.comm.false!!(lemma_ab)
+        let lemma_ba = Nat.lte.succ_left!!(lemma_ba)
         Pair.new!!(Nat.Order.refl(a), lemma_ba)
   }: (lemma_ab: Equal<Bool>(Nat.lte(a, b), cmp_ab)) -> And<
     Equal<Bool>(Nat.lte(a, case cmp_ab { true: b, false: a }), true),
diff --git a/base/Nat/max/combine.kind b/base/Nat/max/combine.kind
new file mode 100644
index 00000000..23b5cf91
--- /dev/null
+++ b/base/Nat/max/combine.kind
@@ -0,0 +1,22 @@
+Nat.max.combine.right(
+  a: Nat
+  b: Nat
+  c: Nat
+  Hyp: Equal<Bool>(Nat.lte(a, b), true)
+): Equal<Bool>(Nat.lte(a, Nat.max(b, c)), true)
+  Nat.Order.chain!!!(Hyp, Nat.max.big.left(b, c))
+
+Nat.max.combine.left(
+  a: Nat
+  b: Nat
+  c: Nat
+  Hyp0: Equal<Bool>(Nat.lte(a, b), true)
+  Hyp1: Equal<Bool>(Nat.lte(c, b), true)
+): Equal<Bool>(Nat.lte(Nat.max(a, c), b), true)
+  def cmp_ac = Nat.lte(a, c)
+  case cmp_ac {
+    true:
+      Hyp1
+    false:
+      Hyp0
+  }! :: Equal<Bool>(Nat.lte(cmp_ac(() Nat, c, a), b), true)
diff --git a/base/Nat/max/comm.kind b/base/Nat/max/comm.kind
index f797e18c..bc4cff16 100644
--- a/base/Nat/max/comm.kind
+++ b/base/Nat/max/comm.kind
@@ -6,6 +6,7 @@ Nat.max.comm(
   case lemma {
     fst:
       let lemma_ba = Nat.lte.comm.false!!(lemma.value)
+      let lemma_ba = Nat.lte.succ_left!!(lemma_ba)
       let qed = Equal.refl<Nat>(a)
       let qed = Equal.rewrite<Bool>(
         false, Nat.lte(a, b), mirror(lemma.value),
@@ -28,6 +29,7 @@ Nat.max.comm(
       qed
     trd:
       let lemma_ab = Nat.lte.comm.false!!(lemma.value)
+      let lemma_ab = Nat.lte.succ_left!!(lemma_ab)
       let qed = Equal.refl<Nat>(b)
       let qed = Equal.rewrite<Bool>(
         false, Nat.lte(b, a), mirror(lemma.value),
diff --git a/base/Nat/max/split.kind b/base/Nat/max/split.kind
new file mode 100644
index 00000000..9935fb19
--- /dev/null
+++ b/base/Nat/max/split.kind
@@ -0,0 +1,8 @@
+Nat.max.split.left(
+  a: Nat
+  b: Nat
+  c: Nat
+  Hyp: Equal<Bool>(Nat.lte(Nat.max(a, b), c), true)
+): And<Equal<Bool>(Nat.lte(a, c), true), Equal<Bool>(Nat.lte(b, c), true)>
+  let {left_lemma, right_lemma} = Nat.max.big(a, b)
+  {Nat.Order.chain!!!(left_lemma, Hyp), Nat.Order.chain!!!(right_lemma, Hyp)}
diff --git a/base/Test.kind b/base/Test.kind
index 49fc720e..15735099 100644
--- a/base/Test.kind
+++ b/base/Test.kind
@@ -1,141 +1,16 @@
-type Nat.AddExp {
-  const(value: Nat)
-  var(idx: Nat)
-  add(left: Nat.AddExp, right: Nat.AddExp)
-}
-
-Nat.AddExp.dimension(
-  exp: Nat.AddExp
-): Nat
-  case exp {
-    const:
-      0
-    add:
-      let left_dim = Nat.AddExp.dimension(exp.left)
-      let right_dim = Nat.AddExp.dimension(exp.right)
-      Nat.max(left_dim, right_dim)
-    var:
-      Nat.succ(exp.idx)
-  }
-
-Nat.AddExp.constant(exp: Nat.AddExp): Type
-  case exp {
-    const:
-      Unit
-    var:
-      Empty
-    add:
-      And<Nat.AddExp.constant(exp.left), Nat.AddExp.constant(exp.right)>
-  }
-
-Nat.AddExp.dimension.zero(
-  exp: Nat.AddExp
-  Hyp: Equal<Nat>(Nat.AddExp.dimension(exp), 0)
-): Nat.AddExp.constant(exp)
-  (case exp {
-    const:
-      (Hyp)
-        unit
-    var:
-      (Hyp)
-        let contra = Nat.succ_neq_zero!(Hyp)
-        Empty.absurd!(contra)
-    add:
-      (Hyp)
-        let {left_small, right_small} = Nat.max.big(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
-        def max = Nat.max(Nat.AddExp.dimension(exp.left), Nat.AddExp.dimension(exp.right))
-        let left_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
-          max, 0, Hyp,
-          (x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.left), x), true),
-          left_small
-        ))
-        let right_zero = Nat.Order.chain.aux!(Equal.rewrite<Nat>(
-          max, 0, Hyp
-          (x) Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp.right), x), true),
-          right_small
-        ))
-        let left = Nat.AddExp.dimension.zero(exp.left, left_zero)
-        let right = Nat.AddExp.dimension.zero(exp.right, right_zero)
-        Pair.new!!(left, right)
-  }: (Hyp: Equal<Nat>(Nat.AddExp.dimension(exp), 0)) -> Nat.AddExp.constant(exp))(
-    Hyp
-  )
-
-Nat.AddExp.compute(
-  exp: Nat.AddExp
-  Hyp: Nat.AddExp.constant(exp)
-): Nat
-  case exp with Hyp {
-    const:
-      exp.value
-    var:
-      Empty.absurd!(Hyp)
-    add:
-      open Hyp
-      Nat.add(Nat.AddExp.compute(exp.left, Hyp.fst), Nat.AddExp.compute(exp.right, Hyp.snd))
-  }!
-
-Nat.AddExp.substitution(
-  exp: Nat.AddExp
-): Variadic(Nat.AddExp.dimension(exp), Nat, Nat)
-  def dim = Nat.AddExp.dimension(exp)
-  def Hyp = Nat.Order.refl(dim)
-  Nat.AddExp.substitution.aux0(dim, exp, Hyp)
-
-Nat.AddExp.substitution.aux0(
-  n: Nat
-  exp: Nat.AddExp
-  Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), n), true)
-): Variadic(n, Nat, Nat)
-  case n with Hyp {
-    zero:
-      def Hyp = Nat.Order.chain.aux!(Hyp)
-      def Hyp = Nat.AddExp.dimension.zero!(Hyp)
-      Nat.AddExp.compute(exp, Hyp)
-    succ:
-      (value)
-        def new_exp = Nat.AddExp.substitution.aux1(exp, value, Nat.succ(n.pred))
-        let Hyp = Nat.AddExp.substitution.aux2(exp, value, Nat.succ(n.pred), Hyp)
-        Nat.AddExp.substitution.aux0(n.pred, new_exp, Hyp)
-  }!
-
-Nat.AddExp.substitution.aux1(
-  exp: Nat.AddExp
-  value: Nat
-  idx: Nat
-): Nat.AddExp
-  case exp {
-    const:
-      exp
-    var:
-      case Nat.lte(idx, exp.idx) {
-        true:
-          Nat.AddExp.const(value)
-        false:
-          exp
-      }
-    add:
-      Nat.AddExp.add(
-        Nat.AddExp.substitution.aux1(exp.left, value, idx)
-        Nat.AddExp.substitution.aux1(exp.right, value, idx)
-      )
-  }
-
-Nat.AddExp.substitution.aux2(
-  exp: Nat.AddExp
-  value: Nat
-  idx: Nat
-  Hyp: Equal<Bool>(Nat.lte(Nat.AddExp.dimension(exp), idx), true)
-): let new_exp = Nat.AddExp.substitution.aux1(exp, value, idx)
-   Equal<Bool>(Nat.lte(Nat.AddExp.dimension(new_exp), Nat.pred(idx)), true)
-  case exp with Hyp {
-    const:
-      Equal.refl<Bool>(true)
-    var:
-      ?var
-    add:
-      ?add
-  }!
-
-Test: _
-  "hi"
+Test<A: Type, B: Type>(
+  f: A -> B,
+  Hyp: (
+    C: Type
+    g: B -> C
+    h: B -> C
+    a: A
+    HHyp: g(f(a)) == h(f(a))
+    b: B
+  ) -> g(b) == h(b)
+  target: B
+): [a: A] f(a) == target
+  let g = ((b) true) :: B -> Bool
+  let h = ((b) Decidable([a: A] f(a) == b)) :: B -> Bool
+  let hmm = Hyp(Type, g, h)
+  ?test