diff --git a/coq/bbencode.v b/coq/bbencode.v
index b795d31..144680f 100644
--- a/coq/bbencode.v
+++ b/coq/bbencode.v
@@ -69,7 +69,7 @@ Compute (expr_subst "x"
 Example  example_let_reduction :
     e1 -->β  (expr_app (expr_app (expr_var "+") bb_zero) bb_zero).
 Proof.
-    apply E_AppLet.
+    apply E_Let.
 Qed.
 
 Compute     (expr_app bb_succ bb_zero) -->β bb_one.
diff --git a/coq/smallstep.v b/coq/smallstep.v
index 2a88c99..16d45c9 100644
--- a/coq/smallstep.v
+++ b/coq/smallstep.v
@@ -61,8 +61,8 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
     e -->β e' ->
     (expr_ty_app e τ) -->β (expr_ty_app e' τ)
 
-  | E_TypAppLam : forall x e a,
-    (expr_ty_app (expr_ty_abs x e) a) -->β (expr_specialize x a e)
+  | E_TypAppLam : forall α e τ,
+    (expr_ty_app (expr_ty_abs α e) τ) -->β (expr_specialize α τ e)
 
   | E_AppLam : forall x τ e a,
     (expr_app (expr_abs x τ e) a) -->β (expr_subst x a e)
@@ -70,8 +70,25 @@ Inductive beta_step : expr_term -> expr_term -> Prop :=
   | E_AppMorph : forall x τ e a,
     (expr_app (expr_morph x τ e) a) -->β (expr_subst x a e)
 
-  | E_AppLet : forall x t e a,
-    (expr_let x t a e) -->β (expr_subst x a e)
+  | E_Let : forall x e a,
+    (expr_let x a e) -->β (expr_subst x a e)
+
+  | E_StripAscend : forall τ e,
+    (expr_ascend τ e) -->β e
+
+  | E_StripDescend : forall τ e,
+    (expr_descend τ e) -->β e
+
+  | E_Ascend : forall τ e e',
+    (e -->β e') ->
+    (expr_ascend τ e) -->β (expr_ascend τ e')
+
+  | E_AscendCollapse : forall τ' τ e,
+    (expr_ascend τ' (expr_ascend τ e)) -->β (expr_ascend (type_ladder τ' τ) e)
+
+  | E_DescendCollapse : forall τ' τ e,
+    (τ':<=τ) ->
+    (expr_descend τ (expr_descend τ' e)) -->β (expr_descend τ e)
 
 where "s '-->β' t" := (beta_step s t).
 
@@ -85,4 +102,43 @@ Inductive multi {X : Type} (R : X -> X -> Prop) : X -> X -> Prop :=
 Notation " s -->α* t " := (multi expr_alpha s t) (at level 40).
 Notation " s -->β* t " := (multi beta_step s t) (at level 40).
 
+
+
+Example reduce1 :
+  [{
+    let "deg2turns" :=
+       (λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
+                ↦morph ((%"/"% (%"x"% des $"ℝ"$) %"360"%) as $"Angle"$~$"Turns"$))
+    in ( %"deg2turns"% (%"60"% as $"Angle"$~$"Degrees"$) )
+  }]
+  -->β*
+  [{
+     ((%"/"% %"60"%) %"360"%) as $"Angle"$~$"Turns"$
+  }].
+Proof.
+  apply Multi_Step with (y:=[{ (λ"x" $"Angle"$~$"Degrees"$~$"ℝ"$
+                ↦morph (((%"/"% (%"x"% des $"ℝ"$)) %"360"%) as $"Angle"$~$"Turns"$)) (%"60"% as $"Angle"$~$"Degrees"$) }]).
+  apply E_Let.
+
+  apply Multi_Step with (y:=(expr_subst "x" [{%"60"% as $"Angle"$~$"Degrees"$}]  [{ (((%"/"% (%"x"% des $"ℝ"$)) %"360"%) as $"Angle"$~$"Turns"$) }])).
+  apply E_AppMorph.
+  simpl.
+
+  apply Multi_Step with (y:=[{ ((%"/"% (%"60"% as $"Angle"$~$"Degrees"$)) %"360"%) as $"Angle"$~$"Turns"$ }]).
+  apply E_Ascend.
+  apply E_App1.
+  apply E_App2.
+  apply V_Abs, VAbs_Var.
+  apply E_StripDescend.
+
+  apply Multi_Step with (y:=[{ (%"/"% %"60"% %"360"%) as $"Angle"$~$"Turns"$ }]).
+  apply E_Ascend.
+  apply E_App1.
+  apply E_App2.
+  apply V_Abs, VAbs_Var.
+  apply E_StripAscend.
+
+  apply Multi_Refl.
+Qed.
+
 End Smallstep.
diff --git a/coq/terms.v b/coq/terms.v
index 1e38a9d..a60a2c1 100644
--- a/coq/terms.v
+++ b/coq/terms.v
@@ -97,6 +97,8 @@ Notation "'let' x ':=' e 'in' t" := (expr_let x e t)
   (in custom ladder_expr at level 20, x constr, e custom ladder_expr at level 99, t custom ladder_expr at level 99) : ladder_expr_scope.
 Notation "e 'as' τ" := (expr_ascend τ e)
   (in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
+Notation "e 'des' τ" := (expr_descend τ e)
+  (in custom ladder_expr at level 30, e custom ladder_expr, τ custom ladder_type at level 99) : ladder_expr_scope.
 Notation "e1 e2" := (expr_app e1 e2)
   (in custom ladder_expr at level 50) : ladder_expr_scope.
 Notation "'(' e ')'" := e