Add appify10

Grrrrrr, code duplication for ladderstep

16 files changed, 509 insertions, 0 deletions

diff --git a/src/Specific/GF25519.v b/src/Specific/GF25519.v
index 361cc83a7..fea289d78 100644
--- a/src/Specific/GF25519.v
+++ b/src/Specific/GF25519.v
@@ -197,6 +197,26 @@ Proof.
   repeat (etransitivity; [ apply app_10_correct | ]); reflexivity.
 Qed.
 
+Definition appify10 {T} (op : fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe25519) :=
+  app_10 x0 (fun x0' =>
+  app_10 x1 (fun x1' =>
+  app_10 x2 (fun x2' =>
+  app_10 x3 (fun x3' =>
+  app_10 x4 (fun x4' =>
+  app_10 x5 (fun x5' =>
+  app_10 x6 (fun x6' =>
+  app_10 x7 (fun x7' =>
+  app_10 x8 (fun x8' =>
+  app_10 x9 (fun x9' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+    @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+Proof.
+  intros. cbv [appify10].
+  repeat (etransitivity; [ apply app_10_correct | ]); reflexivity.
+Qed.
+
 Definition uncurry_unop_fe25519 {T} (op : fe25519 -> T)
   := Eval compute in Tuple.uncurry (n:=length_fe25519) op.
 Definition curry_unop_fe25519 {T} op : fe25519 -> T
@@ -230,6 +250,13 @@ Definition curry_9op_fe25519 {T} op : fe25519 -> fe25519 -> fe25519 -> fe25519 -
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe25519 {T} (op : fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> T)
+  := Eval compute in uncurry_n_op_fe25519 10 op.
+Definition curry_10op_fe25519 {T} op : fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> fe25519 -> T
+  := Eval compute in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+               => curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 (curry_unop_fe25519 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition add_sig (f g : fe25519) :
   { fg : fe25519 | fg = add_opt f g}.
 Proof.
diff --git a/src/Specific/GF25519BoundedCommon.v b/src/Specific/GF25519BoundedCommon.v
index 683f5f47f..bc9118da0 100644
--- a/src/Specific/GF25519BoundedCommon.v
+++ b/src/Specific/GF25519BoundedCommon.v
@@ -206,6 +206,26 @@ Section generic_destructuring.
     intros. cbv [appify9].
     repeat (etransitivity; [ apply app_fe25519W_correct | ]); reflexivity.
   Qed.
+
+  Definition appify10 {T} (op : fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe25519W) :=
+    app_fe25519W x0 (fun x0' =>
+    app_fe25519W x1 (fun x1' =>
+    app_fe25519W x2 (fun x2' =>
+    app_fe25519W x3 (fun x3' =>
+    app_fe25519W x4 (fun x4' =>
+    app_fe25519W x5 (fun x5' =>
+    app_fe25519W x6 (fun x6' =>
+    app_fe25519W x7 (fun x7' =>
+    app_fe25519W x8 (fun x8' =>
+    app_fe25519W x9 (fun x9' =>
+                       op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+  Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+      @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+  Proof.
+    intros. cbv [appify10].
+    repeat (etransitivity; [ apply app_fe25519W_correct | ]); reflexivity.
+  Qed.
 End generic_destructuring.
 
 Definition eta_fe25519W_sig (x : fe25519W) : { v : fe25519W | v = x }.
@@ -406,6 +426,24 @@ Definition curry_9op_fe25519W {T} op : fe25519W -> fe25519W -> fe25519W -> fe255
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe25519W {T} (op : fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> T)
+  := Eval cbv (*-[word64]*) in
+      uncurry_unop_fe25519W (fun x0 =>
+      uncurry_unop_fe25519W (fun x1 =>
+      uncurry_unop_fe25519W (fun x2 =>
+      uncurry_unop_fe25519W (fun x3 =>
+      uncurry_unop_fe25519W (fun x4 =>
+      uncurry_unop_fe25519W (fun x5 =>
+      uncurry_unop_fe25519W (fun x6 =>
+      uncurry_unop_fe25519W (fun x7 =>
+      uncurry_unop_fe25519W (fun x8 =>
+      uncurry_unop_fe25519W (fun x9 =>
+                               op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))).
+Definition curry_10op_fe25519W {T} op : fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> fe25519W -> T
+  := Eval cbv (*-[word64]*) in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+                => curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W (curry_unop_fe25519W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition proj1_fe25519W (x : fe25519) : fe25519W
   := Eval app_tuple_map in
       app_fe25519 x (HList.mapt (fun _ => (@proj_word _ _))).
diff --git a/src/SpecificGen/GF2213_32.v b/src/SpecificGen/GF2213_32.v
index 9b8f0d74e..71e51ccac 100644
--- a/src/SpecificGen/GF2213_32.v
+++ b/src/SpecificGen/GF2213_32.v
@@ -196,6 +196,26 @@ Proof.
   repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
 Qed.
 
+Definition appify10 {T} (op : fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe2213_32) :=
+  app_n x0 (fun x0' =>
+  app_n x1 (fun x1' =>
+  app_n x2 (fun x2' =>
+  app_n x3 (fun x3' =>
+  app_n x4 (fun x4' =>
+  app_n x5 (fun x5' =>
+  app_n x6 (fun x6' =>
+  app_n x7 (fun x7' =>
+  app_n x8 (fun x8' =>
+  app_n x9 (fun x9' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+    @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+Proof.
+  intros. cbv [appify10].
+  repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
 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
@@ -229,6 +249,13 @@ Definition curry_9op_fe2213_32 {T} op : fe2213_32 -> fe2213_32 -> fe2213_32 -> f
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe2213_32 {T} (op : fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> T)
+  := Eval compute in uncurry_n_op_fe2213_32 10 op.
+Definition curry_10op_fe2213_32 {T} op : fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> fe2213_32 -> T
+  := Eval compute in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+               => curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 (curry_unop_fe2213_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition add_sig (f g : fe2213_32) :
   { fg : fe2213_32 | fg = add_opt f g}.
 Proof.
diff --git a/src/SpecificGen/GF2213_32BoundedCommon.v b/src/SpecificGen/GF2213_32BoundedCommon.v
index f9b215ac9..7ec291046 100644
--- a/src/SpecificGen/GF2213_32BoundedCommon.v
+++ b/src/SpecificGen/GF2213_32BoundedCommon.v
@@ -206,6 +206,26 @@ Section generic_destructuring.
     intros. cbv [appify9].
     repeat (etransitivity; [ apply app_fe2213_32W_correct | ]); reflexivity.
   Qed.
+
+  Definition appify10 {T} (op : fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe2213_32W) :=
+    app_fe2213_32W x0 (fun x0' =>
+    app_fe2213_32W x1 (fun x1' =>
+    app_fe2213_32W x2 (fun x2' =>
+    app_fe2213_32W x3 (fun x3' =>
+    app_fe2213_32W x4 (fun x4' =>
+    app_fe2213_32W x5 (fun x5' =>
+    app_fe2213_32W x6 (fun x6' =>
+    app_fe2213_32W x7 (fun x7' =>
+    app_fe2213_32W x8 (fun x8' =>
+    app_fe2213_32W x9 (fun x9' =>
+                       op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+  Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+      @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+  Proof.
+    intros. cbv [appify10].
+    repeat (etransitivity; [ apply app_fe2213_32W_correct | ]); reflexivity.
+  Qed.
 End generic_destructuring.
 
 Definition eta_fe2213_32W_sig (x : fe2213_32W) : { v : fe2213_32W | v = x }.
@@ -406,6 +426,24 @@ Definition curry_9op_fe2213_32W {T} op : fe2213_32W -> fe2213_32W -> fe2213_32W
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe2213_32W {T} (op : fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> T)
+  := Eval cbv (*-[word64]*) in
+      uncurry_unop_fe2213_32W (fun x0 =>
+      uncurry_unop_fe2213_32W (fun x1 =>
+      uncurry_unop_fe2213_32W (fun x2 =>
+      uncurry_unop_fe2213_32W (fun x3 =>
+      uncurry_unop_fe2213_32W (fun x4 =>
+      uncurry_unop_fe2213_32W (fun x5 =>
+      uncurry_unop_fe2213_32W (fun x6 =>
+      uncurry_unop_fe2213_32W (fun x7 =>
+      uncurry_unop_fe2213_32W (fun x8 =>
+      uncurry_unop_fe2213_32W (fun x9 =>
+                               op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))).
+Definition curry_10op_fe2213_32W {T} op : fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> fe2213_32W -> T
+  := Eval cbv (*-[word64]*) in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+                => curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W (curry_unop_fe2213_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition proj1_fe2213_32W (x : fe2213_32) : fe2213_32W
   := Eval app_tuple_map in
       app_fe2213_32 x (HList.mapt (fun _ => (@proj_word _ _))).
diff --git a/src/SpecificGen/GF2519_32.v b/src/SpecificGen/GF2519_32.v
index 72c686596..a9cba3ce0 100644
--- a/src/SpecificGen/GF2519_32.v
+++ b/src/SpecificGen/GF2519_32.v
@@ -196,6 +196,26 @@ Proof.
   repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
 Qed.
 
+Definition appify10 {T} (op : fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe2519_32) :=
+  app_n x0 (fun x0' =>
+  app_n x1 (fun x1' =>
+  app_n x2 (fun x2' =>
+  app_n x3 (fun x3' =>
+  app_n x4 (fun x4' =>
+  app_n x5 (fun x5' =>
+  app_n x6 (fun x6' =>
+  app_n x7 (fun x7' =>
+  app_n x8 (fun x8' =>
+  app_n x9 (fun x9' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+    @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+Proof.
+  intros. cbv [appify10].
+  repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
 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
@@ -229,6 +249,13 @@ Definition curry_9op_fe2519_32 {T} op : fe2519_32 -> fe2519_32 -> fe2519_32 -> f
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe2519_32 {T} (op : fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> T)
+  := Eval compute in uncurry_n_op_fe2519_32 10 op.
+Definition curry_10op_fe2519_32 {T} op : fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> fe2519_32 -> T
+  := Eval compute in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+               => curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 (curry_unop_fe2519_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition add_sig (f g : fe2519_32) :
   { fg : fe2519_32 | fg = add_opt f g}.
 Proof.
diff --git a/src/SpecificGen/GF2519_32BoundedCommon.v b/src/SpecificGen/GF2519_32BoundedCommon.v
index f6bf77cb0..42f7e2610 100644
--- a/src/SpecificGen/GF2519_32BoundedCommon.v
+++ b/src/SpecificGen/GF2519_32BoundedCommon.v
@@ -206,6 +206,26 @@ Section generic_destructuring.
     intros. cbv [appify9].
     repeat (etransitivity; [ apply app_fe2519_32W_correct | ]); reflexivity.
   Qed.
+
+  Definition appify10 {T} (op : fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe2519_32W) :=
+    app_fe2519_32W x0 (fun x0' =>
+    app_fe2519_32W x1 (fun x1' =>
+    app_fe2519_32W x2 (fun x2' =>
+    app_fe2519_32W x3 (fun x3' =>
+    app_fe2519_32W x4 (fun x4' =>
+    app_fe2519_32W x5 (fun x5' =>
+    app_fe2519_32W x6 (fun x6' =>
+    app_fe2519_32W x7 (fun x7' =>
+    app_fe2519_32W x8 (fun x8' =>
+    app_fe2519_32W x9 (fun x9' =>
+                       op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+  Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+      @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+  Proof.
+    intros. cbv [appify10].
+    repeat (etransitivity; [ apply app_fe2519_32W_correct | ]); reflexivity.
+  Qed.
 End generic_destructuring.
 
 Definition eta_fe2519_32W_sig (x : fe2519_32W) : { v : fe2519_32W | v = x }.
@@ -406,6 +426,24 @@ Definition curry_9op_fe2519_32W {T} op : fe2519_32W -> fe2519_32W -> fe2519_32W
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe2519_32W {T} (op : fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> T)
+  := Eval cbv (*-[word64]*) in
+      uncurry_unop_fe2519_32W (fun x0 =>
+      uncurry_unop_fe2519_32W (fun x1 =>
+      uncurry_unop_fe2519_32W (fun x2 =>
+      uncurry_unop_fe2519_32W (fun x3 =>
+      uncurry_unop_fe2519_32W (fun x4 =>
+      uncurry_unop_fe2519_32W (fun x5 =>
+      uncurry_unop_fe2519_32W (fun x6 =>
+      uncurry_unop_fe2519_32W (fun x7 =>
+      uncurry_unop_fe2519_32W (fun x8 =>
+      uncurry_unop_fe2519_32W (fun x9 =>
+                               op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))).
+Definition curry_10op_fe2519_32W {T} op : fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> fe2519_32W -> T
+  := Eval cbv (*-[word64]*) in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+                => curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W (curry_unop_fe2519_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition proj1_fe2519_32W (x : fe2519_32) : fe2519_32W
   := Eval app_tuple_map in
       app_fe2519_32 x (HList.mapt (fun _ => (@proj_word _ _))).
diff --git a/src/SpecificGen/GF25519_32.v b/src/SpecificGen/GF25519_32.v
index 2221c9860..c57fd6786 100644
--- a/src/SpecificGen/GF25519_32.v
+++ b/src/SpecificGen/GF25519_32.v
@@ -196,6 +196,26 @@ Proof.
   repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
 Qed.
 
+Definition appify10 {T} (op : fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe25519_32) :=
+  app_n x0 (fun x0' =>
+  app_n x1 (fun x1' =>
+  app_n x2 (fun x2' =>
+  app_n x3 (fun x3' =>
+  app_n x4 (fun x4' =>
+  app_n x5 (fun x5' =>
+  app_n x6 (fun x6' =>
+  app_n x7 (fun x7' =>
+  app_n x8 (fun x8' =>
+  app_n x9 (fun x9' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+    @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+Proof.
+  intros. cbv [appify10].
+  repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
 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
@@ -229,6 +249,13 @@ Definition curry_9op_fe25519_32 {T} op : fe25519_32 -> fe25519_32 -> fe25519_32
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe25519_32 {T} (op : fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> T)
+  := Eval compute in uncurry_n_op_fe25519_32 10 op.
+Definition curry_10op_fe25519_32 {T} op : fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> fe25519_32 -> T
+  := Eval compute in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+               => curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 (curry_unop_fe25519_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition add_sig (f g : fe25519_32) :
   { fg : fe25519_32 | fg = add_opt f g}.
 Proof.
diff --git a/src/SpecificGen/GF25519_32BoundedCommon.v b/src/SpecificGen/GF25519_32BoundedCommon.v
index bf76e028b..f28608623 100644
--- a/src/SpecificGen/GF25519_32BoundedCommon.v
+++ b/src/SpecificGen/GF25519_32BoundedCommon.v
@@ -206,6 +206,26 @@ Section generic_destructuring.
     intros. cbv [appify9].
     repeat (etransitivity; [ apply app_fe25519_32W_correct | ]); reflexivity.
   Qed.
+
+  Definition appify10 {T} (op : fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe25519_32W) :=
+    app_fe25519_32W x0 (fun x0' =>
+    app_fe25519_32W x1 (fun x1' =>
+    app_fe25519_32W x2 (fun x2' =>
+    app_fe25519_32W x3 (fun x3' =>
+    app_fe25519_32W x4 (fun x4' =>
+    app_fe25519_32W x5 (fun x5' =>
+    app_fe25519_32W x6 (fun x6' =>
+    app_fe25519_32W x7 (fun x7' =>
+    app_fe25519_32W x8 (fun x8' =>
+    app_fe25519_32W x9 (fun x9' =>
+                       op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+  Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+      @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+  Proof.
+    intros. cbv [appify10].
+    repeat (etransitivity; [ apply app_fe25519_32W_correct | ]); reflexivity.
+  Qed.
 End generic_destructuring.
 
 Definition eta_fe25519_32W_sig (x : fe25519_32W) : { v : fe25519_32W | v = x }.
@@ -406,6 +426,24 @@ Definition curry_9op_fe25519_32W {T} op : fe25519_32W -> fe25519_32W -> fe25519_
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe25519_32W {T} (op : fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> T)
+  := Eval cbv (*-[word64]*) in
+      uncurry_unop_fe25519_32W (fun x0 =>
+      uncurry_unop_fe25519_32W (fun x1 =>
+      uncurry_unop_fe25519_32W (fun x2 =>
+      uncurry_unop_fe25519_32W (fun x3 =>
+      uncurry_unop_fe25519_32W (fun x4 =>
+      uncurry_unop_fe25519_32W (fun x5 =>
+      uncurry_unop_fe25519_32W (fun x6 =>
+      uncurry_unop_fe25519_32W (fun x7 =>
+      uncurry_unop_fe25519_32W (fun x8 =>
+      uncurry_unop_fe25519_32W (fun x9 =>
+                               op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))).
+Definition curry_10op_fe25519_32W {T} op : fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> fe25519_32W -> T
+  := Eval cbv (*-[word64]*) in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+                => curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W (curry_unop_fe25519_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition proj1_fe25519_32W (x : fe25519_32) : fe25519_32W
   := Eval app_tuple_map in
       app_fe25519_32 x (HList.mapt (fun _ => (@proj_word _ _))).
diff --git a/src/SpecificGen/GF25519_64.v b/src/SpecificGen/GF25519_64.v
index 6aa576fa4..80d679b73 100644
--- a/src/SpecificGen/GF25519_64.v
+++ b/src/SpecificGen/GF25519_64.v
@@ -196,6 +196,26 @@ Proof.
   repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
 Qed.
 
+Definition appify10 {T} (op : fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe25519_64) :=
+  app_n x0 (fun x0' =>
+  app_n x1 (fun x1' =>
+  app_n x2 (fun x2' =>
+  app_n x3 (fun x3' =>
+  app_n x4 (fun x4' =>
+  app_n x5 (fun x5' =>
+  app_n x6 (fun x6' =>
+  app_n x7 (fun x7' =>
+  app_n x8 (fun x8' =>
+  app_n x9 (fun x9' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+    @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+Proof.
+  intros. cbv [appify10].
+  repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
 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
@@ -229,6 +249,13 @@ Definition curry_9op_fe25519_64 {T} op : fe25519_64 -> fe25519_64 -> fe25519_64
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe25519_64 {T} (op : fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> T)
+  := Eval compute in uncurry_n_op_fe25519_64 10 op.
+Definition curry_10op_fe25519_64 {T} op : fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> fe25519_64 -> T
+  := Eval compute in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+               => curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 (curry_unop_fe25519_64 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition add_sig (f g : fe25519_64) :
   { fg : fe25519_64 | fg = add_opt f g}.
 Proof.
diff --git a/src/SpecificGen/GF25519_64BoundedCommon.v b/src/SpecificGen/GF25519_64BoundedCommon.v
index b4c8e47ca..519b90fac 100644
--- a/src/SpecificGen/GF25519_64BoundedCommon.v
+++ b/src/SpecificGen/GF25519_64BoundedCommon.v
@@ -206,6 +206,26 @@ Section generic_destructuring.
     intros. cbv [appify9].
     repeat (etransitivity; [ apply app_fe25519_64W_correct | ]); reflexivity.
   Qed.
+
+  Definition appify10 {T} (op : fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe25519_64W) :=
+    app_fe25519_64W x0 (fun x0' =>
+    app_fe25519_64W x1 (fun x1' =>
+    app_fe25519_64W x2 (fun x2' =>
+    app_fe25519_64W x3 (fun x3' =>
+    app_fe25519_64W x4 (fun x4' =>
+    app_fe25519_64W x5 (fun x5' =>
+    app_fe25519_64W x6 (fun x6' =>
+    app_fe25519_64W x7 (fun x7' =>
+    app_fe25519_64W x8 (fun x8' =>
+    app_fe25519_64W x9 (fun x9' =>
+                       op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+  Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+      @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+  Proof.
+    intros. cbv [appify10].
+    repeat (etransitivity; [ apply app_fe25519_64W_correct | ]); reflexivity.
+  Qed.
 End generic_destructuring.
 
 Definition eta_fe25519_64W_sig (x : fe25519_64W) : { v : fe25519_64W | v = x }.
@@ -406,6 +426,24 @@ Definition curry_9op_fe25519_64W {T} op : fe25519_64W -> fe25519_64W -> fe25519_
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe25519_64W {T} (op : fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> T)
+  := Eval cbv (*-[word128]*) in
+      uncurry_unop_fe25519_64W (fun x0 =>
+      uncurry_unop_fe25519_64W (fun x1 =>
+      uncurry_unop_fe25519_64W (fun x2 =>
+      uncurry_unop_fe25519_64W (fun x3 =>
+      uncurry_unop_fe25519_64W (fun x4 =>
+      uncurry_unop_fe25519_64W (fun x5 =>
+      uncurry_unop_fe25519_64W (fun x6 =>
+      uncurry_unop_fe25519_64W (fun x7 =>
+      uncurry_unop_fe25519_64W (fun x8 =>
+      uncurry_unop_fe25519_64W (fun x9 =>
+                               op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))).
+Definition curry_10op_fe25519_64W {T} op : fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> fe25519_64W -> T
+  := Eval cbv (*-[word128]*) in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+                => curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W (curry_unop_fe25519_64W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition proj1_fe25519_64W (x : fe25519_64) : fe25519_64W
   := Eval app_tuple_map in
       app_fe25519_64 x (HList.mapt (fun _ => (@proj_word _ _))).
diff --git a/src/SpecificGen/GF41417_32.v b/src/SpecificGen/GF41417_32.v
index 6899f940e..d9d2a871c 100644
--- a/src/SpecificGen/GF41417_32.v
+++ b/src/SpecificGen/GF41417_32.v
@@ -196,6 +196,26 @@ Proof.
   repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
 Qed.
 
+Definition appify10 {T} (op : fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe41417_32) :=
+  app_n x0 (fun x0' =>
+  app_n x1 (fun x1' =>
+  app_n x2 (fun x2' =>
+  app_n x3 (fun x3' =>
+  app_n x4 (fun x4' =>
+  app_n x5 (fun x5' =>
+  app_n x6 (fun x6' =>
+  app_n x7 (fun x7' =>
+  app_n x8 (fun x8' =>
+  app_n x9 (fun x9' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+    @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+Proof.
+  intros. cbv [appify10].
+  repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
 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
@@ -229,6 +249,13 @@ Definition curry_9op_fe41417_32 {T} op : fe41417_32 -> fe41417_32 -> fe41417_32
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe41417_32 {T} (op : fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> T)
+  := Eval compute in uncurry_n_op_fe41417_32 10 op.
+Definition curry_10op_fe41417_32 {T} op : fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> fe41417_32 -> T
+  := Eval compute in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+               => curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 (curry_unop_fe41417_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition add_sig (f g : fe41417_32) :
   { fg : fe41417_32 | fg = add_opt f g}.
 Proof.
diff --git a/src/SpecificGen/GF41417_32BoundedCommon.v b/src/SpecificGen/GF41417_32BoundedCommon.v
index 2bf69d425..5d9a7d209 100644
--- a/src/SpecificGen/GF41417_32BoundedCommon.v
+++ b/src/SpecificGen/GF41417_32BoundedCommon.v
@@ -206,6 +206,26 @@ Section generic_destructuring.
     intros. cbv [appify9].
     repeat (etransitivity; [ apply app_fe41417_32W_correct | ]); reflexivity.
   Qed.
+
+  Definition appify10 {T} (op : fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe41417_32W) :=
+    app_fe41417_32W x0 (fun x0' =>
+    app_fe41417_32W x1 (fun x1' =>
+    app_fe41417_32W x2 (fun x2' =>
+    app_fe41417_32W x3 (fun x3' =>
+    app_fe41417_32W x4 (fun x4' =>
+    app_fe41417_32W x5 (fun x5' =>
+    app_fe41417_32W x6 (fun x6' =>
+    app_fe41417_32W x7 (fun x7' =>
+    app_fe41417_32W x8 (fun x8' =>
+    app_fe41417_32W x9 (fun x9' =>
+                       op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+  Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+      @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+  Proof.
+    intros. cbv [appify10].
+    repeat (etransitivity; [ apply app_fe41417_32W_correct | ]); reflexivity.
+  Qed.
 End generic_destructuring.
 
 Definition eta_fe41417_32W_sig (x : fe41417_32W) : { v : fe41417_32W | v = x }.
@@ -406,6 +426,24 @@ Definition curry_9op_fe41417_32W {T} op : fe41417_32W -> fe41417_32W -> fe41417_
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe41417_32W {T} (op : fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> T)
+  := Eval cbv (*-[word64]*) in
+      uncurry_unop_fe41417_32W (fun x0 =>
+      uncurry_unop_fe41417_32W (fun x1 =>
+      uncurry_unop_fe41417_32W (fun x2 =>
+      uncurry_unop_fe41417_32W (fun x3 =>
+      uncurry_unop_fe41417_32W (fun x4 =>
+      uncurry_unop_fe41417_32W (fun x5 =>
+      uncurry_unop_fe41417_32W (fun x6 =>
+      uncurry_unop_fe41417_32W (fun x7 =>
+      uncurry_unop_fe41417_32W (fun x8 =>
+      uncurry_unop_fe41417_32W (fun x9 =>
+                               op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))).
+Definition curry_10op_fe41417_32W {T} op : fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> fe41417_32W -> T
+  := Eval cbv (*-[word64]*) in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+                => curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W (curry_unop_fe41417_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition proj1_fe41417_32W (x : fe41417_32) : fe41417_32W
   := Eval app_tuple_map in
       app_fe41417_32 x (HList.mapt (fun _ => (@proj_word _ _))).
diff --git a/src/SpecificGen/GF5211_32.v b/src/SpecificGen/GF5211_32.v
index 6b9f360c8..edc1bc979 100644
--- a/src/SpecificGen/GF5211_32.v
+++ b/src/SpecificGen/GF5211_32.v
@@ -196,6 +196,26 @@ Proof.
   repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
 Qed.
 
+Definition appify10 {T} (op : fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe5211_32) :=
+  app_n x0 (fun x0' =>
+  app_n x1 (fun x1' =>
+  app_n x2 (fun x2' =>
+  app_n x3 (fun x3' =>
+  app_n x4 (fun x4' =>
+  app_n x5 (fun x5' =>
+  app_n x6 (fun x6' =>
+  app_n x7 (fun x7' =>
+  app_n x8 (fun x8' =>
+  app_n x9 (fun x9' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+    @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+Proof.
+  intros. cbv [appify10].
+  repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
 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
@@ -229,6 +249,13 @@ Definition curry_9op_fe5211_32 {T} op : fe5211_32 -> fe5211_32 -> fe5211_32 -> f
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe5211_32 {T} (op : fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> T)
+  := Eval compute in uncurry_n_op_fe5211_32 10 op.
+Definition curry_10op_fe5211_32 {T} op : fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> fe5211_32 -> T
+  := Eval compute in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+               => curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 (curry_unop_fe5211_32 op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition add_sig (f g : fe5211_32) :
   { fg : fe5211_32 | fg = add_opt f g}.
 Proof.
diff --git a/src/SpecificGen/GF5211_32BoundedCommon.v b/src/SpecificGen/GF5211_32BoundedCommon.v
index 20e8c84fd..7ca03193f 100644
--- a/src/SpecificGen/GF5211_32BoundedCommon.v
+++ b/src/SpecificGen/GF5211_32BoundedCommon.v
@@ -206,6 +206,26 @@ Section generic_destructuring.
     intros. cbv [appify9].
     repeat (etransitivity; [ apply app_fe5211_32W_correct | ]); reflexivity.
   Qed.
+
+  Definition appify10 {T} (op : fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe5211_32W) :=
+    app_fe5211_32W x0 (fun x0' =>
+    app_fe5211_32W x1 (fun x1' =>
+    app_fe5211_32W x2 (fun x2' =>
+    app_fe5211_32W x3 (fun x3' =>
+    app_fe5211_32W x4 (fun x4' =>
+    app_fe5211_32W x5 (fun x5' =>
+    app_fe5211_32W x6 (fun x6' =>
+    app_fe5211_32W x7 (fun x7' =>
+    app_fe5211_32W x8 (fun x8' =>
+    app_fe5211_32W x9 (fun x9' =>
+                       op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+  Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+      @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+  Proof.
+    intros. cbv [appify10].
+    repeat (etransitivity; [ apply app_fe5211_32W_correct | ]); reflexivity.
+  Qed.
 End generic_destructuring.
 
 Definition eta_fe5211_32W_sig (x : fe5211_32W) : { v : fe5211_32W | v = x }.
@@ -406,6 +426,24 @@ Definition curry_9op_fe5211_32W {T} op : fe5211_32W -> fe5211_32W -> fe5211_32W
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_fe5211_32W {T} (op : fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> T)
+  := Eval cbv (*-[word64]*) in
+      uncurry_unop_fe5211_32W (fun x0 =>
+      uncurry_unop_fe5211_32W (fun x1 =>
+      uncurry_unop_fe5211_32W (fun x2 =>
+      uncurry_unop_fe5211_32W (fun x3 =>
+      uncurry_unop_fe5211_32W (fun x4 =>
+      uncurry_unop_fe5211_32W (fun x5 =>
+      uncurry_unop_fe5211_32W (fun x6 =>
+      uncurry_unop_fe5211_32W (fun x7 =>
+      uncurry_unop_fe5211_32W (fun x8 =>
+      uncurry_unop_fe5211_32W (fun x9 =>
+                               op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9)))))))))).
+Definition curry_10op_fe5211_32W {T} op : fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> fe5211_32W -> T
+  := Eval cbv (*-[word64]*) in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+                => curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W (curry_unop_fe5211_32W op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition proj1_fe5211_32W (x : fe5211_32) : fe5211_32W
   := Eval app_tuple_map in
       app_fe5211_32 x (HList.mapt (fun _ => (@proj_word _ _))).
diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4
index a9d6c574f..5d3b9c263 100644
--- a/src/SpecificGen/GFtemplate3mod4
+++ b/src/SpecificGen/GFtemplate3mod4
@@ -196,6 +196,26 @@ Proof.
   repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
 Qed.
 
+Definition appify10 {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}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe{{{k}}}{{{c}}}_{{{w}}}) :=
+  app_n x0 (fun x0' =>
+  app_n x1 (fun x1' =>
+  app_n x2 (fun x2' =>
+  app_n x3 (fun x3' =>
+  app_n x4 (fun x4' =>
+  app_n x5 (fun x5' =>
+  app_n x6 (fun x6' =>
+  app_n x7 (fun x7' =>
+  app_n x8 (fun x8' =>
+  app_n x9 (fun x9' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+    @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+Proof.
+  intros. cbv [appify10].
+  repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
 Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> T)
   := 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
@@ -229,6 +249,13 @@ Definition curry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}}
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_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}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T)
+  := Eval compute in uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} 10 op.
+Definition curry_10op_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}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T
+  := Eval compute in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+               => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
   { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = add_opt f g}.
 Proof.
diff --git a/src/SpecificGen/GFtemplate5mod8 b/src/SpecificGen/GFtemplate5mod8
index c0ad5a630..579be07bf 100644
--- a/src/SpecificGen/GFtemplate5mod8
+++ b/src/SpecificGen/GFtemplate5mod8
@@ -196,6 +196,26 @@ Proof.
   repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
 Qed.
 
+Definition appify10 {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}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T) (x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 : fe{{{k}}}{{{c}}}_{{{w}}}) :=
+  app_n x0 (fun x0' =>
+  app_n x1 (fun x1' =>
+  app_n x2 (fun x2' =>
+  app_n x3 (fun x3' =>
+  app_n x4 (fun x4' =>
+  app_n x5 (fun x5' =>
+  app_n x6 (fun x6' =>
+  app_n x7 (fun x7' =>
+  app_n x8 (fun x8' =>
+  app_n x9 (fun x9' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8' x9')))))))))).
+
+Lemma appify10_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9,
+    @appify10 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9 = op x0 x1 x2 x3 x4 x5 x6 x7 x8 x9.
+Proof.
+  intros. cbv [appify10].
+  repeat (etransitivity; [ apply app_n_correct | ]); reflexivity.
+Qed.
+
 Definition uncurry_unop_fe{{{k}}}{{{c}}}_{{{w}}} {T} (op : fe{{{k}}}{{{c}}}_{{{w}}} -> T)
   := 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
@@ -229,6 +249,13 @@ Definition curry_9op_fe{{{k}}}{{{c}}}_{{{w}}} {T} op : fe{{{k}}}{{{c}}}_{{{w}}}
       appify9 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8
                => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8).
 
+Definition uncurry_10op_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}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T)
+  := Eval compute in uncurry_n_op_fe{{{k}}}{{{c}}}_{{{w}}} 10 op.
+Definition curry_10op_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}}} -> fe{{{k}}}{{{c}}}_{{{w}}} -> T
+  := Eval compute in
+      appify10 (fun x0 x1 x2 x3 x4 x5 x6 x7 x8 x9
+               => curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} (curry_unop_fe{{{k}}}{{{c}}}_{{{w}}} op x0) x1) x2) x3) x4) x5) x6) x7) x8) x9).
+
 Definition add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
   { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = add_opt f g}.
 Proof.