uncurry_n_op_fe25519

14 files changed, 246 insertions, 258 deletions

diff --git a/src/SpecificGen/GF2213_32.v b/src/SpecificGen/GF2213_32.v
index cd5ff40c5..9b8f0d74e 100644
--- a/src/SpecificGen/GF2213_32.v
+++ b/src/SpecificGen/GF2213_32.v
@@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Tower.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Algebra.
@@ -199,8 +200,20 @@ Definition uncurry_unop_fe2213_32 {T} (op : fe2213_32 -> T)
   := Eval compute in Tuple.uncurry (n:=length_fe2213_32) op.
 Definition curry_unop_fe2213_32 {T} op : fe2213_32 -> T
   := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe2213_32) op).
+
+Fixpoint uncurry_n_op_fe2213_32 {T} n
+  : forall (op : Tower.tower_nd fe2213_32 T n),
+    Tower.tower_nd Z T (n * length_fe2213_32)
+  := match n
+           return (forall (op : Tower.tower_nd fe2213_32 T n),
+                      Tower.tower_nd Z T (n * length_fe2213_32))
+     with
+     | O => fun x => x
+     | S n' => fun f => uncurry_unop_fe2213_32 (fun x => @uncurry_n_op_fe2213_32 _ n' (f x))
+     end.
+
 Definition uncurry_binop_fe2213_32 {T} (op : fe2213_32 -> fe2213_32 -> T)
-  := Eval compute in uncurry_unop_fe2213_32 (fun f => uncurry_unop_fe2213_32 (op f)).
+  := Eval compute in uncurry_n_op_fe2213_32 2 op.
 Definition curry_binop_fe2213_32 {T} op : fe2213_32 -> fe2213_32 -> T
   := Eval compute in appify2 (fun f => curry_unop_fe2213_32 (curry_unop_fe2213_32 op f)).
 
@@ -210,17 +223,7 @@ Definition curry_unop_wire_digits {T} op : wire_digits -> T
   := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
 
 Definition uncurry_9op_fe2213_32 {T} (op : fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> T)
-  := Eval compute in
-      uncurry_unop_fe2213_32 (fun x0 =>
-      uncurry_unop_fe2213_32 (fun x1 =>
-      uncurry_unop_fe2213_32 (fun x2 =>
-      uncurry_unop_fe2213_32 (fun x3 =>
-      uncurry_unop_fe2213_32 (fun x4 =>
-      uncurry_unop_fe2213_32 (fun x5 =>
-      uncurry_unop_fe2213_32 (fun x6 =>
-      uncurry_unop_fe2213_32 (fun x7 =>
-      uncurry_unop_fe2213_32 (fun x8 =>
-                               op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+  := Eval compute in uncurry_n_op_fe2213_32 9 op.
 Definition curry_9op_fe2213_32 {T} op : fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> T
   := Eval compute in
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v
index 52f488f2e..e5fab2a8d 100644
--- a/src/SpecificGen/GF2213_32Reflective/Common.v
+++ b/src/SpecificGen/GF2213_32Reflective/Common.v
@@ -98,10 +98,10 @@ Local Ltac bounds_from_list_cps ls :=
                         constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra))
   end.
 
-Local Ltac make_bounds_cps ls :=
+Local Ltac make_bounds_cps ls extra :=
   let v := bounds_from_list_cps (List.rev ls) in
   let v := (eval compute in v) in
-  pose v.
+  exact (v _ extra).
 
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
@@ -116,36 +116,30 @@ Local Ltac make_bounds ls :=
   let v := (eval compute in v) in
   exact v.
 
-(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
+Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
 Proof.
   refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with
          | 0 => tt
-         | S n => let v := Expr_nm_Op_bounds n count_out in
-                  _
+         | S n => let v := interp_all_binders_for_to' (Expr_nm_Op_bounds n count_out) in
+                  interp_all_binders_for_of' _
          end; simpl.
-  make_bounds_cps (Tuple.to_list _ bounds).
-  pose (p _ v).
-  repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]).
-  exact p0.
-*)
-Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined.
-Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
-Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
-Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
+  make_bounds_cps (Tuple.to_list _ bounds) v.
+Defined.
+Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 2 1.
+Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 4 1.
+Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 9 4.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
-Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type.
-Proof.
-  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 4)).
-Defined.
-Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type.
-Proof.
-  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 9)).
-Defined.
+
 Definition interp_bexpr : ExprBinOp -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
   := fun e => curry_binop_fe2213_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W -> SpecificGen.GF2213_32BoundedCommon.fe2213_32W
@@ -512,7 +506,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe2213_32WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
diff --git a/src/SpecificGen/GF2519_32.v b/src/SpecificGen/GF2519_32.v
index 98338b64c..72c686596 100644
--- a/src/SpecificGen/GF2519_32.v
+++ b/src/SpecificGen/GF2519_32.v
@@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Tower.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Algebra.
@@ -199,8 +200,20 @@ Definition uncurry_unop_fe2519_32 {T} (op : fe2519_32 -> T)
   := Eval compute in Tuple.uncurry (n:=length_fe2519_32) op.
 Definition curry_unop_fe2519_32 {T} op : fe2519_32 -> T
   := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe2519_32) op).
+
+Fixpoint uncurry_n_op_fe2519_32 {T} n
+  : forall (op : Tower.tower_nd fe2519_32 T n),
+    Tower.tower_nd Z T (n * length_fe2519_32)
+  := match n
+           return (forall (op : Tower.tower_nd fe2519_32 T n),
+                      Tower.tower_nd Z T (n * length_fe2519_32))
+     with
+     | O => fun x => x
+     | S n' => fun f => uncurry_unop_fe2519_32 (fun x => @uncurry_n_op_fe2519_32 _ n' (f x))
+     end.
+
 Definition uncurry_binop_fe2519_32 {T} (op : fe2519_32 -> fe2519_32 -> T)
-  := Eval compute in uncurry_unop_fe2519_32 (fun f => uncurry_unop_fe2519_32 (op f)).
+  := Eval compute in uncurry_n_op_fe2519_32 2 op.
 Definition curry_binop_fe2519_32 {T} op : fe2519_32 -> fe2519_32 -> T
   := Eval compute in appify2 (fun f => curry_unop_fe2519_32 (curry_unop_fe2519_32 op f)).
 
@@ -210,17 +223,7 @@ Definition curry_unop_wire_digits {T} op : wire_digits -> T
   := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
 
 Definition uncurry_9op_fe2519_32 {T} (op : fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> T)
-  := Eval compute in
-      uncurry_unop_fe2519_32 (fun x0 =>
-      uncurry_unop_fe2519_32 (fun x1 =>
-      uncurry_unop_fe2519_32 (fun x2 =>
-      uncurry_unop_fe2519_32 (fun x3 =>
-      uncurry_unop_fe2519_32 (fun x4 =>
-      uncurry_unop_fe2519_32 (fun x5 =>
-      uncurry_unop_fe2519_32 (fun x6 =>
-      uncurry_unop_fe2519_32 (fun x7 =>
-      uncurry_unop_fe2519_32 (fun x8 =>
-                               op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+  := Eval compute in uncurry_n_op_fe2519_32 9 op.
 Definition curry_9op_fe2519_32 {T} op : fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> T
   := Eval compute in
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v
index 4be893f8f..729c79995 100644
--- a/src/SpecificGen/GF2519_32Reflective/Common.v
+++ b/src/SpecificGen/GF2519_32Reflective/Common.v
@@ -98,10 +98,10 @@ Local Ltac bounds_from_list_cps ls :=
                         constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra))
   end.
 
-Local Ltac make_bounds_cps ls :=
+Local Ltac make_bounds_cps ls extra :=
   let v := bounds_from_list_cps (List.rev ls) in
   let v := (eval compute in v) in
-  pose v.
+  exact (v _ extra).
 
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
@@ -116,36 +116,30 @@ Local Ltac make_bounds ls :=
   let v := (eval compute in v) in
   exact v.
 
-(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
+Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
 Proof.
   refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with
          | 0 => tt
-         | S n => let v := Expr_nm_Op_bounds n count_out in
-                  _
+         | S n => let v := interp_all_binders_for_to' (Expr_nm_Op_bounds n count_out) in
+                  interp_all_binders_for_of' _
          end; simpl.
-  make_bounds_cps (Tuple.to_list _ bounds).
-  pose (p _ v).
-  repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]).
-  exact p0.
-*)
-Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined.
-Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
-Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
-Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
+  make_bounds_cps (Tuple.to_list _ bounds) v.
+Defined.
+Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 2 1.
+Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 4 1.
+Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 9 4.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
-Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type.
-Proof.
-  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 4)).
-Defined.
-Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type.
-Proof.
-  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 9)).
-Defined.
+
 Definition interp_bexpr : ExprBinOp -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
   := fun e => curry_binop_fe2519_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W -> SpecificGen.GF2519_32BoundedCommon.fe2519_32W
@@ -512,7 +506,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe2519_32WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
diff --git a/src/SpecificGen/GF25519_32.v b/src/SpecificGen/GF25519_32.v
index 89f63a572..2221c9860 100644
--- a/src/SpecificGen/GF25519_32.v
+++ b/src/SpecificGen/GF25519_32.v
@@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Tower.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Algebra.
@@ -199,8 +200,20 @@ Definition uncurry_unop_fe25519_32 {T} (op : fe25519_32 -> T)
   := Eval compute in Tuple.uncurry (n:=length_fe25519_32) op.
 Definition curry_unop_fe25519_32 {T} op : fe25519_32 -> T
   := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe25519_32) op).
+
+Fixpoint uncurry_n_op_fe25519_32 {T} n
+  : forall (op : Tower.tower_nd fe25519_32 T n),
+    Tower.tower_nd Z T (n * length_fe25519_32)
+  := match n
+           return (forall (op : Tower.tower_nd fe25519_32 T n),
+                      Tower.tower_nd Z T (n * length_fe25519_32))
+     with
+     | O => fun x => x
+     | S n' => fun f => uncurry_unop_fe25519_32 (fun x => @uncurry_n_op_fe25519_32 _ n' (f x))
+     end.
+
 Definition uncurry_binop_fe25519_32 {T} (op : fe25519_32 -> fe25519_32 -> T)
-  := Eval compute in uncurry_unop_fe25519_32 (fun f => uncurry_unop_fe25519_32 (op f)).
+  := Eval compute in uncurry_n_op_fe25519_32 2 op.
 Definition curry_binop_fe25519_32 {T} op : fe25519_32 -> fe25519_32 -> T
   := Eval compute in appify2 (fun f => curry_unop_fe25519_32 (curry_unop_fe25519_32 op f)).
 
@@ -210,17 +223,7 @@ Definition curry_unop_wire_digits {T} op : wire_digits -> T
   := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
 
 Definition uncurry_9op_fe25519_32 {T} (op : fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> T)
-  := Eval compute in
-      uncurry_unop_fe25519_32 (fun x0 =>
-      uncurry_unop_fe25519_32 (fun x1 =>
-      uncurry_unop_fe25519_32 (fun x2 =>
-      uncurry_unop_fe25519_32 (fun x3 =>
-      uncurry_unop_fe25519_32 (fun x4 =>
-      uncurry_unop_fe25519_32 (fun x5 =>
-      uncurry_unop_fe25519_32 (fun x6 =>
-      uncurry_unop_fe25519_32 (fun x7 =>
-      uncurry_unop_fe25519_32 (fun x8 =>
-                               op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+  := Eval compute in uncurry_n_op_fe25519_32 9 op.
 Definition curry_9op_fe25519_32 {T} op : fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> T
   := Eval compute in
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v
index 3389f908a..aad67f032 100644
--- a/src/SpecificGen/GF25519_32Reflective/Common.v
+++ b/src/SpecificGen/GF25519_32Reflective/Common.v
@@ -98,10 +98,10 @@ Local Ltac bounds_from_list_cps ls :=
                         constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra))
   end.
 
-Local Ltac make_bounds_cps ls :=
+Local Ltac make_bounds_cps ls extra :=
   let v := bounds_from_list_cps (List.rev ls) in
   let v := (eval compute in v) in
-  pose v.
+  exact (v _ extra).
 
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
@@ -116,36 +116,30 @@ Local Ltac make_bounds ls :=
   let v := (eval compute in v) in
   exact v.
 
-(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
+Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
 Proof.
   refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with
          | 0 => tt
-         | S n => let v := Expr_nm_Op_bounds n count_out in
-                  _
+         | S n => let v := interp_all_binders_for_to' (Expr_nm_Op_bounds n count_out) in
+                  interp_all_binders_for_of' _
          end; simpl.
-  make_bounds_cps (Tuple.to_list _ bounds).
-  pose (p _ v).
-  repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]).
-  exact p0.
-*)
-Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined.
-Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
-Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
-Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
+  make_bounds_cps (Tuple.to_list _ bounds) v.
+Defined.
+Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 2 1.
+Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 4 1.
+Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 9 4.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
-Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type.
-Proof.
-  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 4)).
-Defined.
-Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type.
-Proof.
-  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 9)).
-Defined.
+
 Definition interp_bexpr : ExprBinOp -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
   := fun e => curry_binop_fe25519_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W -> SpecificGen.GF25519_32BoundedCommon.fe25519_32W
@@ -512,7 +506,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe25519_32WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
diff --git a/src/SpecificGen/GF25519_64.v b/src/SpecificGen/GF25519_64.v
index 3645a59f7..6aa576fa4 100644
--- a/src/SpecificGen/GF25519_64.v
+++ b/src/SpecificGen/GF25519_64.v
@@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Tower.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Algebra.
@@ -199,8 +200,20 @@ Definition uncurry_unop_fe25519_64 {T} (op : fe25519_64 -> T)
   := Eval compute in Tuple.uncurry (n:=length_fe25519_64) op.
 Definition curry_unop_fe25519_64 {T} op : fe25519_64 -> T
   := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe25519_64) op).
+
+Fixpoint uncurry_n_op_fe25519_64 {T} n
+  : forall (op : Tower.tower_nd fe25519_64 T n),
+    Tower.tower_nd Z T (n * length_fe25519_64)
+  := match n
+           return (forall (op : Tower.tower_nd fe25519_64 T n),
+                      Tower.tower_nd Z T (n * length_fe25519_64))
+     with
+     | O => fun x => x
+     | S n' => fun f => uncurry_unop_fe25519_64 (fun x => @uncurry_n_op_fe25519_64 _ n' (f x))
+     end.
+
 Definition uncurry_binop_fe25519_64 {T} (op : fe25519_64 -> fe25519_64 -> T)
-  := Eval compute in uncurry_unop_fe25519_64 (fun f => uncurry_unop_fe25519_64 (op f)).
+  := Eval compute in uncurry_n_op_fe25519_64 2 op.
 Definition curry_binop_fe25519_64 {T} op : fe25519_64 -> fe25519_64 -> T
   := Eval compute in appify2 (fun f => curry_unop_fe25519_64 (curry_unop_fe25519_64 op f)).
 
@@ -210,17 +223,7 @@ Definition curry_unop_wire_digits {T} op : wire_digits -> T
   := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
 
 Definition uncurry_9op_fe25519_64 {T} (op : fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> T)
-  := Eval compute in
-      uncurry_unop_fe25519_64 (fun x0 =>
-      uncurry_unop_fe25519_64 (fun x1 =>
-      uncurry_unop_fe25519_64 (fun x2 =>
-      uncurry_unop_fe25519_64 (fun x3 =>
-      uncurry_unop_fe25519_64 (fun x4 =>
-      uncurry_unop_fe25519_64 (fun x5 =>
-      uncurry_unop_fe25519_64 (fun x6 =>
-      uncurry_unop_fe25519_64 (fun x7 =>
-      uncurry_unop_fe25519_64 (fun x8 =>
-                               op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+  := Eval compute in uncurry_n_op_fe25519_64 9 op.
 Definition curry_9op_fe25519_64 {T} op : fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> T
   := Eval compute in
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v
index bbdccaf26..f639aa0b6 100644
--- a/src/SpecificGen/GF25519_64Reflective/Common.v
+++ b/src/SpecificGen/GF25519_64Reflective/Common.v
@@ -98,10 +98,10 @@ Local Ltac bounds_from_list_cps ls :=
                         constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra))
   end.
 
-Local Ltac make_bounds_cps ls :=
+Local Ltac make_bounds_cps ls extra :=
   let v := bounds_from_list_cps (List.rev ls) in
   let v := (eval compute in v) in
-  pose v.
+  exact (v _ extra).
 
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
@@ -116,36 +116,30 @@ Local Ltac make_bounds ls :=
   let v := (eval compute in v) in
   exact v.
 
-(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
+Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
 Proof.
   refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with
          | 0 => tt
-         | S n => let v := Expr_nm_Op_bounds n count_out in
-                  _
+         | S n => let v := interp_all_binders_for_to' (Expr_nm_Op_bounds n count_out) in
+                  interp_all_binders_for_of' _
          end; simpl.
-  make_bounds_cps (Tuple.to_list _ bounds).
-  pose (p _ v).
-  repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]).
-  exact p0.
-*)
-Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined.
-Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
-Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
-Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
+  make_bounds_cps (Tuple.to_list _ bounds) v.
+Defined.
+Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 2 1.
+Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 4 1.
+Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 9 4.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
-Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type.
-Proof.
-  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 4)).
-Defined.
-Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type.
-Proof.
-  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 9)).
-Defined.
+
 Definition interp_bexpr : ExprBinOp -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
   := fun e => curry_binop_fe25519_64W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W -> SpecificGen.GF25519_64BoundedCommon.fe25519_64W
@@ -512,7 +506,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe25519_64WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
diff --git a/src/SpecificGen/GF41417_32.v b/src/SpecificGen/GF41417_32.v
index 9d0e73245..6899f940e 100644
--- a/src/SpecificGen/GF41417_32.v
+++ b/src/SpecificGen/GF41417_32.v
@@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Tower.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Algebra.
@@ -199,8 +200,20 @@ Definition uncurry_unop_fe41417_32 {T} (op : fe41417_32 -> T)
   := Eval compute in Tuple.uncurry (n:=length_fe41417_32) op.
 Definition curry_unop_fe41417_32 {T} op : fe41417_32 -> T
   := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe41417_32) op).
+
+Fixpoint uncurry_n_op_fe41417_32 {T} n
+  : forall (op : Tower.tower_nd fe41417_32 T n),
+    Tower.tower_nd Z T (n * length_fe41417_32)
+  := match n
+           return (forall (op : Tower.tower_nd fe41417_32 T n),
+                      Tower.tower_nd Z T (n * length_fe41417_32))
+     with
+     | O => fun x => x
+     | S n' => fun f => uncurry_unop_fe41417_32 (fun x => @uncurry_n_op_fe41417_32 _ n' (f x))
+     end.
+
 Definition uncurry_binop_fe41417_32 {T} (op : fe41417_32 -> fe41417_32 -> T)
-  := Eval compute in uncurry_unop_fe41417_32 (fun f => uncurry_unop_fe41417_32 (op f)).
+  := Eval compute in uncurry_n_op_fe41417_32 2 op.
 Definition curry_binop_fe41417_32 {T} op : fe41417_32 -> fe41417_32 -> T
   := Eval compute in appify2 (fun f => curry_unop_fe41417_32 (curry_unop_fe41417_32 op f)).
 
@@ -210,17 +223,7 @@ Definition curry_unop_wire_digits {T} op : wire_digits -> T
   := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
 
 Definition uncurry_9op_fe41417_32 {T} (op : fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> T)
-  := Eval compute in
-      uncurry_unop_fe41417_32 (fun x0 =>
-      uncurry_unop_fe41417_32 (fun x1 =>
-      uncurry_unop_fe41417_32 (fun x2 =>
-      uncurry_unop_fe41417_32 (fun x3 =>
-      uncurry_unop_fe41417_32 (fun x4 =>
-      uncurry_unop_fe41417_32 (fun x5 =>
-      uncurry_unop_fe41417_32 (fun x6 =>
-      uncurry_unop_fe41417_32 (fun x7 =>
-      uncurry_unop_fe41417_32 (fun x8 =>
-                               op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+  := Eval compute in uncurry_n_op_fe41417_32 9 op.
 Definition curry_9op_fe41417_32 {T} op : fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> T
   := Eval compute in
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v
index 40089d503..62d55b463 100644
--- a/src/SpecificGen/GF41417_32Reflective/Common.v
+++ b/src/SpecificGen/GF41417_32Reflective/Common.v
@@ -98,10 +98,10 @@ Local Ltac bounds_from_list_cps ls :=
                         constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra))
   end.
 
-Local Ltac make_bounds_cps ls :=
+Local Ltac make_bounds_cps ls extra :=
   let v := bounds_from_list_cps (List.rev ls) in
   let v := (eval compute in v) in
-  pose v.
+  exact (v _ extra).
 
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
@@ -116,36 +116,30 @@ Local Ltac make_bounds ls :=
   let v := (eval compute in v) in
   exact v.
 
-(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
+Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
 Proof.
   refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with
          | 0 => tt
-         | S n => let v := Expr_nm_Op_bounds n count_out in
-                  _
+         | S n => let v := interp_all_binders_for_to' (Expr_nm_Op_bounds n count_out) in
+                  interp_all_binders_for_of' _
          end; simpl.
-  make_bounds_cps (Tuple.to_list _ bounds).
-  pose (p _ v).
-  repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]).
-  exact p0.
-*)
-Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined.
-Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
-Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
-Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
+  make_bounds_cps (Tuple.to_list _ bounds) v.
+Defined.
+Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 2 1.
+Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 4 1.
+Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 9 4.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
-Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type.
-Proof.
-  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 4)).
-Defined.
-Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type.
-Proof.
-  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 9)).
-Defined.
+
 Definition interp_bexpr : ExprBinOp -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
   := fun e => curry_binop_fe41417_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W -> SpecificGen.GF41417_32BoundedCommon.fe41417_32W
@@ -512,7 +506,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe41417_32WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
diff --git a/src/SpecificGen/GF5211_32.v b/src/SpecificGen/GF5211_32.v
index 48f85104a..6b9f360c8 100644
--- a/src/SpecificGen/GF5211_32.v
+++ b/src/SpecificGen/GF5211_32.v
@@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Tower.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Algebra.
@@ -199,8 +200,20 @@ Definition uncurry_unop_fe5211_32 {T} (op : fe5211_32 -> T)
   := Eval compute in Tuple.uncurry (n:=length_fe5211_32) op.
 Definition curry_unop_fe5211_32 {T} op : fe5211_32 -> T
   := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe5211_32) op).
+
+Fixpoint uncurry_n_op_fe5211_32 {T} n
+  : forall (op : Tower.tower_nd fe5211_32 T n),
+    Tower.tower_nd Z T (n * length_fe5211_32)
+  := match n
+           return (forall (op : Tower.tower_nd fe5211_32 T n),
+                      Tower.tower_nd Z T (n * length_fe5211_32))
+     with
+     | O => fun x => x
+     | S n' => fun f => uncurry_unop_fe5211_32 (fun x => @uncurry_n_op_fe5211_32 _ n' (f x))
+     end.
+
 Definition uncurry_binop_fe5211_32 {T} (op : fe5211_32 -> fe5211_32 -> T)
-  := Eval compute in uncurry_unop_fe5211_32 (fun f => uncurry_unop_fe5211_32 (op f)).
+  := Eval compute in uncurry_n_op_fe5211_32 2 op.
 Definition curry_binop_fe5211_32 {T} op : fe5211_32 -> fe5211_32 -> T
   := Eval compute in appify2 (fun f => curry_unop_fe5211_32 (curry_unop_fe5211_32 op f)).
 
@@ -210,17 +223,7 @@ Definition curry_unop_wire_digits {T} op : wire_digits -> T
   := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
 
 Definition uncurry_9op_fe5211_32 {T} (op : fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> T)
-  := Eval compute in
-      uncurry_unop_fe5211_32 (fun x0 =>
-      uncurry_unop_fe5211_32 (fun x1 =>
-      uncurry_unop_fe5211_32 (fun x2 =>
-      uncurry_unop_fe5211_32 (fun x3 =>
-      uncurry_unop_fe5211_32 (fun x4 =>
-      uncurry_unop_fe5211_32 (fun x5 =>
-      uncurry_unop_fe5211_32 (fun x6 =>
-      uncurry_unop_fe5211_32 (fun x7 =>
-      uncurry_unop_fe5211_32 (fun x8 =>
-                               op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+  := Eval compute in uncurry_n_op_fe5211_32 9 op.
 Definition curry_9op_fe5211_32 {T} op : fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> T
   := Eval compute in
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v
index 2ad555057..977710173 100644
--- a/src/SpecificGen/GF5211_32Reflective/Common.v
+++ b/src/SpecificGen/GF5211_32Reflective/Common.v
@@ -98,10 +98,10 @@ Local Ltac bounds_from_list_cps ls :=
                         constr:(fun T extra => (Some {| Bounds.lower := fst x ; Bounds.upper := snd x |}, bs T extra))
   end.
 
-Local Ltac make_bounds_cps ls :=
+Local Ltac make_bounds_cps ls extra :=
   let v := bounds_from_list_cps (List.rev ls) in
   let v := (eval compute in v) in
-  pose v.
+  exact (v _ extra).
 
 Local Ltac bounds_from_list ls :=
   lazymatch (eval hnf in ls) with
@@ -116,36 +116,30 @@ Local Ltac make_bounds ls :=
   let v := (eval compute in v) in
   exact v.
 
-(*Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
+Fixpoint Expr_nm_Op_bounds count_in count_out : interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type.
 Proof.
   refine match count_in return interp_all_binders_for (Expr_nm_OpT count_in count_out) ZBounds.interp_base_type with
          | 0 => tt
-         | S n => let v := Expr_nm_Op_bounds n count_out in
-                  _
+         | S n => let v := interp_all_binders_for_to' (Expr_nm_Op_bounds n count_out) in
+                  interp_all_binders_for_of' _
          end; simpl.
-  make_bounds_cps (Tuple.to_list _ bounds).
-  pose (p _ v).
-  repeat (split; [ exact (fst p0) | ]; destruct p0 as [_ p0]).
-  exact p0.
-*)
-Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds ++ Tuple.to_list _ bounds)%list. Defined.
-Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
-Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
-Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type.
-Proof. make_bounds (Tuple.to_list _ bounds). Defined.
+  make_bounds_cps (Tuple.to_list _ bounds) v.
+Defined.
+Definition ExprBinOp_bounds : interp_all_binders_for ExprBinOpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 2 1.
+Definition ExprUnOp_bounds : interp_all_binders_for ExprUnOpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition ExprUnOpFEToZ_bounds : interp_all_binders_for ExprUnOpFEToZT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition ExprUnOpFEToWire_bounds : interp_all_binders_for ExprUnOpFEToWireT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 1 1.
+Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 4 1.
+Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type
+  := Eval compute in Expr_nm_Op_bounds 9 4.
 Definition ExprUnOpWireToFE_bounds : interp_all_binders_for ExprUnOpWireToFET ZBounds.interp_base_type.
 Proof. make_bounds (Tuple.to_list _ wire_digit_bounds). Defined.
-Definition Expr4Op_bounds : interp_all_binders_for Expr4OpT ZBounds.interp_base_type.
-Proof.
-  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 4)).
-Defined.
-Definition Expr9Op_bounds : interp_all_binders_for Expr9_4OpT ZBounds.interp_base_type.
-Proof.
-  make_bounds (List.fold_right (@List.app _) nil (List.repeat (Tuple.to_list _ bounds) 9)).
-Defined.
+
 Definition interp_bexpr : ExprBinOp -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
   := fun e => curry_binop_fe5211_32W (Interp (@WordW.interp_op) e).
 Definition interp_uexpr : ExprUnOp -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W -> SpecificGen.GF5211_32BoundedCommon.fe5211_32W
@@ -512,7 +506,7 @@ Ltac t_correct_and_bounded ropZ_sig Hbounds H0 H1 args :=
   repeat match goal with x := _ |- _ => subst x end;
   cbv [id
          binop_args_to_bounded unop_args_to_bounded unopWireToFE_args_to_bounded op9_args_to_bounded
-         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
+         Relations.proj_eq_rel interp_flat_type_rel_pointwise2 SmartVarfMap interp_flat_type smart_interp_flat_map Application.all_binders_for fst snd BoundedWordW.to_wordW' BoundedWordW.boundedWordToWordW BoundedWord.value Application.ApplyInterpedAll Application.ApplyInterpedAll' Application.interp_all_binders_for_of' Application.interp_all_binders_for_to' Application.fst_binder Application.snd_binder interp_flat_type_rel_pointwise2_gen_Prop Relations.related_wordW_boundsi' Relations.related'_wordW_bounds Bounds.upper Bounds.lower Application.remove_all_binders WordW.to_Z] in Hbounds_left, Hbounds_right;
   lazymatch goal with
   | [ |- fe5211_32WToZ ?x = _ /\ _ ]
     => generalize dependent x; intros
diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4
index bc7766f7a..a9d6c574f 100644
--- a/src/SpecificGen/GFtemplate3mod4
+++ b/src/SpecificGen/GFtemplate3mod4
@@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Tower.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Algebra.
@@ -199,8 +200,20 @@ Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w
   := Eval compute in Tuple.uncurry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op.
 Definition curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> T
   := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op).
+
+Fixpoint uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} {T} n
+  : forall (op : Tower.tower_nd fe{{{k}}}{{{c}}}_{{{w}}} T n),
+    Tower.tower_nd Z T (n * length_fe{{{k}}}{{{c}}}_{{{w}}})
+  := match n
+           return (forall (op : Tower.tower_nd fe{{{k}}}{{{c}}}_{{{w}}} T n),
+                      Tower.tower_nd Z T (n * length_fe{{{k}}}{{{c}}}_{{{w}}}))
+     with
+     | O => fun x => x
+     | S n' => fun f => uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x => @uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} _ n' (f x))
+     end.
+
 Definition uncurry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T)
-  := Eval compute in uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun f => uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (op f)).
+  := Eval compute in uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} 2 op.
 Definition curry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T
   := Eval compute in appify2 (fun f => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op f)).
 
@@ -210,17 +223,7 @@ Definition curry_unop_wire_digits {T} op : wire_digits -> T
   := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
 
 Definition uncurry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T)
-  := Eval compute in
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x0 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x1 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x2 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x3 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x4 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x5 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x6 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x7 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x8 =>
-                               op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+  := Eval compute in uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} 9 op.
 Definition curry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T
   := Eval compute in
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
diff --git a/src/SpecificGen/GFtemplate5mod8 b/src/SpecificGen/GFtemplate5mod8
index 7a0f0f22c..c0ad5a630 100644
--- a/src/SpecificGen/GFtemplate5mod8
+++ b/src/SpecificGen/GFtemplate5mod8
@@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Tower.
 Require Import Crypto.Util.Notations.
 Require Import Crypto.Util.Decidable.
 Require Import Crypto.Algebra.
@@ -199,8 +200,20 @@ Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w
   := Eval compute in Tuple.uncurry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op.
 Definition curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> T
   := Eval compute in fun f => app_n f (Tuple.curry (n:=length_fe{{{k}}}{{{c}}}_{{{w}}}) op).
+
+Fixpoint uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} {T} n
+  : forall (op : Tower.tower_nd fe{{{k}}}{{{c}}}_{{{w}}} T n),
+    Tower.tower_nd Z T (n * length_fe{{{k}}}{{{c}}}_{{{w}}})
+  := match n
+           return (forall (op : Tower.tower_nd fe{{{k}}}{{{c}}}_{{{w}}} T n),
+                      Tower.tower_nd Z T (n * length_fe{{{k}}}{{{c}}}_{{{w}}}))
+     with
+     | O => fun x => x
+     | S n' => fun f => uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x => @uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} _ n' (f x))
+     end.
+
 Definition uncurry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T)
-  := Eval compute in uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun f => uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (op f)).
+  := Eval compute in uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} 2 op.
 Definition curry_binop_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T
   := Eval compute in appify2 (fun f => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op f)).
 
@@ -210,17 +223,7 @@ Definition curry_unop_wire_digits {T} op : wire_digits -> T
   := Eval compute in fun f => app_n2 f (Tuple.curry (n:=length wire_widths) op).
 
 Definition uncurry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T)
-  := Eval compute in
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x0 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x1 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x2 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x3 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x4 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x5 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x6 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x7 =>
-      uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (fun x8 =>
-                               op x0 x1 x2 x3 x4 x5 x6 x7 x8))))))))).
+  := Eval compute in uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} 9 op.
 Definition curry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T
   := Eval compute in
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8