diff --git a/src/lambda/lambda.lisp b/src/lambda/lambda.lisp
index 280d2ecae..ccbee88b6 100644
--- a/src/lambda/lambda.lisp
+++ b/src/lambda/lambda.lisp
@@ -319,13 +319,15 @@ nil"))
                                                    (mapcar #'ttype term)
                                                    :from-end t)
                                            (ttype tterm)))))
-               ((or (plus ltm rtm)
-                    (minus ltm rtm)
-                    (times ltm rtm)
-                    (divide ltm rtm)
-                    (lamb-eq ltm rtm)
-                    (lamb-lt ltm rtm))
-                (obj-equalp (ttype ltm) (ttype rtm)))
+               ((or plus
+                    minus
+                    divide
+                    times)
+                (obj-equalp (ttype (ltm tterm))
+                            (ttype (rtm tterm))))
+               ((or lamb-eq
+                    lamb-lt)
+                t)
                (index t)
                (unit t)
                (err t)
@@ -360,3 +362,321 @@ nil"))
          (or (errorp (ltm tterm))
              (errorp (rtm tterm))))
         (t                        (errorp (term tterm)))))
+
+(defun dispatch (tterm)
+  "A dispatch refering the class of a term to its function"
+  (typecase tterm
+    (absurd #'absurd)
+    (unit   #'unit)
+    (left   #'left)
+    (right   #'right)
+    (case-on #'case-on)
+    (fst #'fst)
+    (snd #'snd)
+    (pair #'pair)
+    (lamb #'lamb)
+    (app #'app)
+    (index #'index)
+    (err #'err)
+    (bit-choice #'bit-choice)
+    (plus #'plus)
+    (minus #'minus)
+    (divide #'divide)
+    (times #'times)
+    (lamb-eq #'lamb-eq)
+    (lamb-lt #'lamb-lt)))
+
+(defun dispatch-arith (tterm)
+  "A dispatch refering the class of an arithmetic term
+to its corresponding operation"
+  (typecase tterm
+    (plus #'+)
+    (minus #'-)
+    (divide #'floor)
+    (times #'*)
+    (lamb-eq #'=)
+    (lamb-lt #'<)))
+
+(defun index-excess (tterm)
+  "Checks all indeces occuring in a term which will be substituted.
+If position exceeds n, adds depth to the index. Necessary for
+beta-substitution of indices which point outside of the app term"
+  (labels ((rec (n tterm)
+             (typecase tterm
+               (absurd    (absurd (tcod tterm)
+                                  (rec n (term tterm))))
+               (left      (left (rty tterm)
+                                (rec n (term tterm))))
+               (right     (right (lty tterm)
+                                 (rec n (term tterm))))
+               (case-on   (case-on (rec n (on tterm))
+                                   (rec (1+ n) (ltm tterm))
+                                   (rec (1+ n) (rtm tterm))))
+               (fst       (fst (rec n (term tterm))))
+               (snd       (snd (rec n (term tterm))))
+               (lamb      (lamb (tdom tterm)
+                                (rec (1+ n) (term tterm))))
+               (app       (app (rec n (fun tterm))
+                               (list (rec n (car (term tterm))))))
+               (index     (if (>= (pos tterm) n)
+                              (index (1+ (pos tterm)))
+                              tterm))
+               ((or unit
+                    err
+                    bit-choice)
+                tterm)
+               ((or plus
+                    times
+                    minus
+                    divide
+                    lamb-eq
+                    lamb-lt
+                    pair)
+                (funcall (dispatch tterm)
+                         (rec n (ltm tterm))
+                         (rec n (rtm tterm)))))))
+    (rec 0 tterm)))
+
+(defun index-lack (n tterm)
+  "Checks if a term has made substitutions and decreases the index
+of term accordingly"
+  (labels ((rec (n tterm)
+             (if (typep tterm 'list)
+                 tterm
+                 (typecase tterm
+                   (absurd    (absurd (tcod tterm)
+                                      (rec n (term tterm))))
+                   (left      (left (rty tterm)
+                                    (rec n (term tterm))))
+                   (right     (right (lty tterm)
+                                     (rec n (term tterm))))
+                   (case-on   (case-on (rec n (on tterm))
+                                       (rec (1+ n) (ltm tterm))
+                                       (rec (1+ n) (rtm tterm))))
+                   (fst       (fst (rec n (term tterm))))
+                   (snd       (snd (rec n (term tterm))))
+                   (lamb      (lamb (tdom tterm)
+                                    (rec (1+ n) (term tterm))))
+                   (app      (app (rec n (fun tterm))
+                                  (list (rec n (car (term tterm))))))
+                   (index     (if (> (pos tterm) n)
+                                  (index (1- (pos tterm)))
+                                  tterm))
+                   ((or unit
+                        err
+                        bit-choice)
+                    tterm)
+                   ((or plus
+                        times
+                        minus
+                        divide
+                        lamb-eq
+                        lamb-lt
+                        pair)
+                    (funcall (dispatch tterm)
+                             (rec n (ltm tterm))
+                             (rec n (rtm tterm))))))))
+    (rec n tterm)))
+
+(defun delist (tterm)
+  "We mark substituted terms by listing them. This function recovers the car
+of the list."
+  (labels ((rec (tterm)
+             (if (typep tterm 'list)
+                 (car tterm)
+                 (typecase tterm
+                   (absurd    (absurd (tcod tterm)
+                                      (rec (term tterm))))
+                   (left      (left (rty tterm)
+                                    (rec (term tterm))))
+                   (right     (right (lty tterm)
+                                     (rec (term tterm))))
+                   (case-on   (case-on (rec (on tterm))
+                                       (rec (ltm tterm))
+                                       (rec (rtm tterm))))
+                   (fst       (fst (rec (term tterm))))
+                   (snd       (snd (rec (term tterm))))
+                   (lamb      (lamb (tdom tterm)
+                                    (rec (term tterm))))
+                   (app      (app (rec (fun tterm))
+                                  (list (rec (car (term tterm))))))
+                   ((or unit
+                        err
+                        index
+                        bit-choice)
+                    tterm)
+                   ((or plus
+                        times
+                        minus
+                        divide
+                        lamb-eq
+                        lamb-lt
+                        pair)
+                    (funcall (dispatch tterm)
+                             (rec (ltm tterm))
+                             (rec (rtm tterm))))))))
+    (rec tterm)))
+
+(defun sub (ind term-to-replace sub-in)
+  "Substitutes the occurence of index (ind) inside of the top
+subterms of sub-on by term-to-replace. We mark replaced terms by
+listing them"
+  (typecase sub-in
+    (absurd   (absurd (tcod sub-in) (sub ind
+                                         term-to-replace
+                                         (term sub-in))))
+    (left     (left (rty sub-in) (sub ind
+                                      term-to-replace
+                                      (term sub-in))))
+    (right     (right (lty sub-in) (sub ind
+                                        term-to-replace
+                                        (term sub-in))))
+    (case-on   (case-on (sub ind
+                             term-to-replace
+                             (on sub-in))
+                        (sub (1+ ind)
+                             (index-excess term-to-replace)
+                             (ltm sub-in))
+                        (sub (1+ ind)
+                             (index-excess term-to-replace)
+                             (rtm sub-in))))
+    (fst        (fst (substitute ind
+                                 term-to-replace
+                                 (term sub-in))))
+    (snd        (snd (substitute ind
+                                 term-to-replace
+                                 (term sub-in))))
+    (lamb      (lamb (tdom sub-in)
+                     (sub (1+ ind)
+                          (index-excess term-to-replace)
+                          (term sub-in))))
+    (app        (app (sub ind term-to-replace (fun sub-in))
+                     (list (sub ind term-to-replace (car (term sub-in))))))
+    (index      (if (= (pos sub-in) ind)
+                    (list term-to-replace)
+                    sub-in))
+    ((or unit
+         err
+         bit-choice)
+     sub-in)
+    ((or plus
+         times
+         minus
+         divide
+         lamb-eq
+         lamb-lt
+         pair)
+     (funcall (dispatch sub-in)
+              (sub ind term-to-replace (ltm sub-in))
+              (sub ind term-to-replace (rtm sub-in))))))
+
+(defun reducer (tterm)
+  "Reduces a given Lambda term by applying explict beta-reduction
+when possible alongside arithmetic simplification. We assume that the
+lambda and app terms are  1-argument"
+  (labels ((rec (tterm) 
+             (typecase tterm
+               (absurd   (absurd (tcod tterm) (rec (term tterm))))
+               (left     (left (rty tterm) (rec (term tterm))))
+               (right    (right (lty tterm) (rec (term tterm))))
+               (case-on  (let ((on (on tterm))
+                               (ltm (ltm tterm))
+                               (rtm (rtm tterm)))
+                           (cond ((typep on 'left)
+                                  (delist (index-lack 0
+                                                      (sub 0 on ltm))))
+                                 ((typep on 'right)
+                                  (delist (index-lack 0
+                                                      (sub 0 on rtm))))
+                                 (t
+                                  (case-on (rec on)
+                                           (rec ltm)
+                                           (rec rtm))))))
+               (pair     (pair (rec (ltm tterm))
+                               (rec (rtm tterm))))
+               (fst      (let ((term (term tterm)))
+                           (if (typep (rec term) 'pair)
+                               (rec (ltm term))
+                               (fst (rec term)))))
+               (snd      (let ((term (term tterm)))
+                           (if (typep (rec term) 'pair)
+                               (rec (rtm term))
+                               (snd (rec term)))))
+               (lamb     (lamb (tdom tterm) (rec (term tterm))))
+               (app      (let ((fun (fun tterm))
+                               (term (car (term tterm))))
+                           (cond ((typep fun 'lamb)
+                                  (delist (index-lack 0
+                                                      (sub 0
+                                                           (rec term)
+                                                           (rec (term fun))))))
+                                 ((and (typep fun 'case-on)
+                                       (typep (ltm fun) 'lamb)
+                                       (typep (rtm fun) 'lamb))
+                                  (let ((irec (index-excess (rec term))))
+                                    (rec (case-on (rec (on fun))
+                                                  (delist
+                                                   (index-lack 0
+                                                               (sub 0 irec
+                                                                    (rec (term (ltm fun))))))
+                                                  (delist
+                                                   (index-lack 0
+                                                               (sub 0 irec
+                                                                    (rec (term (rtm fun))))))))))
+                                 ((and (typep fun 'case-on)
+                                       (typep (ltm fun) 'lamb)
+                                       (typep (rtm fun) 'case-on))
+                                  (rec (case-on (rec (on fun))
+                                                (delist
+                                                 (index-lack 0
+                                                             (sub 0 (index-excess (rec term))
+                                                                  (rec (term (ltm fun))))))
+                                                (rec (app (rtm fun) (list (index-excess term)))))))
+                                 ((and (typep fun 'case-on)
+                                       (typep (ltm fun) 'lamb)
+                                       (typep (rtm fun) 'case-on))
+                                  (rec (case-on (rec (on fun))
+                                                (rec (app (ltm fun) (list (index-excess term))))
+                                                (delist
+                                                 (index-lack 0
+                                                             (sub 0 (index-excess (rec term))
+                                                                  (rec (term (rtm fun)))))))))
+                                 ((typep fun 'err)
+                                  (err (mcadr (ttype fun))))
+                                 (t (app (rec fun) (list (rec term)))))))
+               ((or lamb-eq
+                    lamb-lt)
+                (let ((ltm (ltm tterm))
+                      (rtm (rtm tterm)))
+                  (if (and (typep ltm 'bit-choice)
+                           (typep rtm 'bit-choice))
+                      (if (funcall (dispatch-arith tterm)
+                                   (bitv ltm)
+                                   (bitv rtm))
+                          (left so1 (unit))
+                          (right so1 (unit)))
+                      (funcall (dispatch tterm)
+                               (rec ltm)
+                               (rec rtm)))))
+               ((or plus
+                    times
+                    minus
+                    divide)
+                (let ((ltm (ltm tterm))
+                      (rtm (rtm tterm)))
+                  (if (and (typep ltm 'bit-choice)
+                           (typep rtm 'bit-choice))
+                      (bit-choice
+                       (funcall (dispatch-arith tterm)
+                                (bitv ltm)
+                                (bitv rtm)))
+                      (funcall (dispatch tterm)
+                               (rec ltm)
+                               (rec rtm)))))
+               ((or unit
+                    index
+                    err
+                    bit-choice)
+                tterm))))
+    (rec tterm)))
+
diff --git a/src/lambda/package.lisp b/src/lambda/package.lisp
index eb4ea5039..fc0470723 100644
--- a/src/lambda/package.lisp
+++ b/src/lambda/package.lisp
@@ -27,6 +27,7 @@
   (fun-type           pax:class)
   (fun-type           pax:function)
   (errorp             pax:function)
+  (reducer            pax:function)
 
   (mcar              (pax:method () (fun-type)))
   (mcadr             (pax:method () (fun-type)))
diff --git a/src/lambda/trans.lisp b/src/lambda/trans.lisp
index 7bc48f2cf..f500e54d4 100644
--- a/src/lambda/trans.lisp
+++ b/src/lambda/trans.lisp
@@ -398,68 +398,20 @@ iterated, so is the uncurrying."
                              (comp (funcall op (num (ttype ltm)))
                                    (geb:pair (rec context ltm)
                                              (rec context (rtm tterm))))))
-                    (arith (dispatch tterm))))))))
-    (cond ((not (well-defp context tterm))
-           (error "not a well-defined ~A in said ~A" tterm context))
-          ((typep tterm 'lamb)
-           (rec (append (mapcar #'fun-to-hom (tdom tterm)) context)
-                (ann-term1 (append (mapcar #'fun-to-hom (tdom tterm)) context)
-                           (term tterm))))
-          (t
-           (rec context (ann-term1 context tterm))))))
-
-(defun fun-depth (obj)
-  "Looks at how iterated a function type is with [SUBSTOBJ][GEB.SPEC:SUBSTOBJ]
-being 0 iterated looking at the [MCADR][generic-function]. E.g.:
-
-```lisp
-TRANS> (fun-depth so1)
-0
-
-TRANS> (fun-depth (fun-type so1 so1))
-1
-
-TRANS> (fun-depth (fun-type so1 (fun-type so1 so1)))
-2
-
-TRANS> (fun-depth (fun-type (fun-type so1 so1) so1))
-1
-```"
-  (if (not (typep obj 'fun-type))
-      0
-      (1+ (fun-depth (mcadr obj)))))
-
-(defun fun-uncurry-prod (obj f)
-  "Takes a morphism f : X -> obj where obj is an iterated function type
-represented in Geb as B^(A1 x ... x An) and uncurries it but looking at the
-iteration as product to a morphism f' : (A1 x ... An) x X -> B. E.g:
-
-``lisp
-TRANS> (fun-uncurry-prod (fun-type so1 (fun-type so1 so1)) (init so1))
-(∘ (∘ (∘ (<-left s-1 s-1)
-         ((∘ (<-left s-1 s-1)
-             ((<-left s-1 (× s-1 s-1))
-              (∘ (<-left s-1 s-1) (<-right s-1 (× s-1 s-1)))))
-          (∘ (<-right s-1 s-1) (<-right s-1 (× s-1 s-1)))))
-      ((∘ (0-> s-1) (<-left s-0 (× s-1 s-1))) (<-right s-0 (× s-1 s-1))))
-   ((<-right (× s-1 s-1) s-0) (<-left (× s-1 s-1) s-0)))
-
-TRANS> (dom (fun-uncurry-prod (fun-type so1 (fun-type so1 so1)) (init so1)))
-(× (× s-1 s-1) s-0)
-
-TRANS> (codom (fun-uncurry-prod (fun-type so1 (fun-type so1 so1)) (init so1)))
-s-1
-```"
-  (labels ((lst-mcar (num ob)
-             (if (= num 1)
-                 (list (mcar ob))
-                 (cons (mcar (apply-n (1- num) #'mcadr ob))
-                       (lst-mcar (1- num) ob)))))
-    (commutes-left (uncurry (reduce #'prod
-                                    (lst-mcar (fun-depth obj) obj)
-                                    :from-end t)
-                            (apply-n (fun-depth obj) #'mcadr obj)
-                            f))))
+                    (arith (dispatch tterm)))))))
+           (rec1 (ctx tterm)
+             (if (typep tterm 'lamb)
+                 (rec1 (append (tdom tterm) ctx)
+                       (term tterm))
+                 (list ctx tterm))))
+    (if (not (well-defp context tterm))
+        (error "not a well-defined ~A in said ~A" tterm context)
+        (let* ((term (geb.lambda.main:reducer tterm))
+               (recc (rec1 context term))
+               (car (car recc)))
+          (rec car
+               (ann-term1 car
+                          (cadr recc)))))))
 
 (-> stlc-ctx-to-mu (stlc-context) substobj)
 (defun stlc-ctx-to-mu (context)
diff --git a/src/seqn/trans.lisp b/src/seqn/trans.lisp
index 92bc4f82f..73bf3b9e7 100644
--- a/src/seqn/trans.lisp
+++ b/src/seqn/trans.lisp
@@ -184,7 +184,7 @@ removed already and hence we cannot count as usual"
         (let ((plus (+ (vamp:const car)
                        (vamp:const cadr))))
           (if (> (expt 2 mcar) plus)
-              (vamp:make-constant :const plus)
+              (list (vamp:make-constant :const plus))
               (error "Range Exceeded")))
         (list (geb.vampir:plus-range (vamp:make-constant :const mcar)
                                      car
@@ -197,7 +197,7 @@ removed already and hence we cannot count as usual"
     (if (const-check inputs)
         (let ((minus (- (vamp:const car) (vamp:const cadr))))
           (if (<= 0 minus)
-              (vamp:make-constant :const minus)
+              (list (vamp:make-constant :const minus))
               (error "Subtraction Produces Negative Numbers")))
         (list (geb.vampir:minus-range (vamp:make-constant :const (mcar obj))
                                       car
@@ -211,7 +211,7 @@ removed already and hence we cannot count as usual"
     (if (const-check inputs)
         (let ((mult (* (vamp:const car) (vamp:const cadr))))
           (if (> (expt 2 mcar) mult)
-              (vamp:make-constant :const mult)
+              (list (vamp:make-constant :const mult))
               (error "Range Exceeded")))
         (list (geb.vampir:mult-range (vamp:make-constant :const mcar)
                                      car
@@ -222,9 +222,9 @@ removed already and hence we cannot count as usual"
   (let ((car (car inputs))
         (cadr (cadr inputs)))
     (if (const-check inputs)
-        (vamp:make-constant
-         :const
-         (multiple-value-bind (q) (floor (vamp:const car) (vamp:const cadr)) q))
+        (list  (vamp:make-constant
+                :const
+                (multiple-value-bind (q) (floor (vamp:const car) (vamp:const cadr)) q)))
         (list (vamp:make-infix :op :/
                                :lhs (car inputs)
                                :rhs (cadr inputs))))))
diff --git a/src/specs/lambda.lisp b/src/specs/lambda.lisp
index 1f3ed53a0..56f212f17 100644
--- a/src/specs/lambda.lisp
+++ b/src/specs/lambda.lisp
@@ -65,7 +65,6 @@ $$\\Gamma \\vdash \\text{tcod : Type}$$ and
 $$\\Gamma \\vdash \\text{term : so0}$$ one deduces
 $$\\Gamma \\vdash \\text{(absurd tcod term) : tcod}$$"))
 
-(-> absurd (cat-obj <stlc> &key (:ttype t)) absurd)
 (defun absurd (tcod term &key (ttype nil))
   (values
    (make-instance 'absurd :tcod tcod :term term :ttype ttype)))
@@ -95,7 +94,6 @@ we provide all terms untyped.
 This grammar corresponds to the introduction rule of the unit type. Namely
 $$\\Gamma \\dashv \\text{(unit) : so1}$$"))
 
-(-> unit (&key (:ttype t)) unit)
 (defun unit (&key (ttype nil))
   (values
    (make-instance 'unit :ttype ttype)))
@@ -139,7 +137,6 @@ $$\\Gamma \\dashv \\text{term : (ttype term)}$$ we deduce
 $$\\Gamma \\dashv \\text{(left rty term) : (coprod (ttype term) rty)}$$
 "))
 
-(-> left (cat-obj <stlc> &key (:ttype t)) left)
 (defun left (rty term &key (ttype nil))
   (values
    (make-instance 'left :rty rty :term term :ttype ttype)))
@@ -182,7 +179,6 @@ $$\\Gamma \\dashv \\text{term : (ttype term)}$$ we deduce
 $$\\Gamma \\dashv \\text{(right lty term) : (coprod lty (ttype term))}$$
 "))
 
-(-> right (cat-obj <stlc> &key (:ttype t)) right)
 (defun right (lty term &key (ttype nil))
   (values
    (make-instance 'right :lty lty :term term :ttype ttype)))
@@ -231,7 +227,6 @@ Note that in practice we append contexts on the left as computation of
 [INDEX][class] is done from the left. Otherwise, the rules are the same as in
 usual type theory if context was read from right to left."))
 
-(-> case-on (<stlc> <stlc> <stlc> &key (:ttype t)) case-on)
 (defun case-on (on ltm rtm &key (ttype nil))
   (values
    (make-instance 'case-on :on on :ltm ltm :rtm rtm :ttype ttype)))
@@ -272,7 +267,6 @@ $$\\Gamma \\vdash \\text{rtm : (mcadr (ttype (pair ltm rtm)))}$$ we have
 $$\\Gamma \\vdash \\text{(pair ltm rtm) : (ttype (pair ltm rtm))}$$
 "))
 
-(-> pair (<stlc> <stlc> &key (:ttype t)) pair)
 (defun pair (ltm rtm &key (ttype nil))
   (values
    (make-instance 'pair :ltm ltm :rtm rtm :ttype ttype)))
@@ -306,7 +300,6 @@ we are projecting to.
 This corresponds to the first projection function gotten by induction
 on a term of a product type."))
 
-(-> fst (<stlc> &key (:ttype t)) fst)
 (defun fst (term &key (ttype nil))
   (values
    (make-instance 'fst :term term :ttype ttype)))
@@ -340,7 +333,6 @@ part we are projecting to.
 This corresponds to the second projection function gotten by induction
 on a term of a product type."))
 
-(-> snd (<stlc> &key (:ttype t)) snd)
 (defun snd (term &key (ttype nil))
   (values
    (make-instance 'snd :term term :ttype ttype)))
@@ -429,7 +421,6 @@ the left. Note that in practice we append contexts on the left as computation of
 [INDEX][class] is done from the left. Otherwise, the rules are the same as in
 usual type theory if context was read from right to left."))
 
-(-> lamb (list <stlc> &key (:ttype t)) lamb)
 (defun lamb (tdom term &key (ttype nil))
   (values
    (make-instance 'lamb :tdom tdom :term term :ttype ttype)))
@@ -495,7 +486,6 @@ G ⊢ (app f t₁ ··· tₙ₋₁) : Aₙ
 Note again that i'th term should correspond to the ith element of the product
 in the codomain counted from the left."))
 
-(-> app (<stlc> list &key (:ttype t)) app)
 (defun app (fun term &key (ttype nil))
   (values
     (make-instance 'app :fun fun :term term :ttype ttype)))
@@ -533,7 +523,6 @@ $$\\Gamma_1 , \\ldots , \\Gamma_k \\vdash \\text{(index pos) :} \\Gamma_{pos}$$
 Note that we add contexts on the left rather than on the right contra classical
 type-theoretic notation."))
 
-(-> index (fixnum &key (:ttype t)) index)
 (defun index (pos &key (ttype nil))
   (values
    (make-instance 'index :pos pos :ttype ttype)))
@@ -556,7 +545,6 @@ currently having no particular feedback but with functionality to be of an
 arbitrary type. Note that this is the only STLC term class which does not
 have [TTYPE][generic-function] a possibly empty accessor."))
 
-(-> err (cat-obj) err)
 (defun err (ttype)
   (values
    (make-instance 'err :ttype ttype)))