Update AddCoordinates

Now the _correct_and_bounded lemma goes through

8 files changed, 288 insertions, 0 deletions

diff --git a/src/SpecificGen/GF2213_32.v b/src/SpecificGen/GF2213_32.v
index 87da8dbcc..cd5ff40c5 100644
--- a/src/SpecificGen/GF2213_32.v
+++ b/src/SpecificGen/GF2213_32.v
@@ -176,6 +176,25 @@ Proof.
   etransitivity; apply app_n_correct.
 Qed.
 
+Definition appify9 {T} (op : 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 : 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' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+    @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+  intros. cbv [appify9].
+  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
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
 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))))))))).
+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
+               => 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 add_sig (f g : fe2213_32) :
   { fg : fe2213_32 | fg = add_opt f g}.
 Proof.
diff --git a/src/SpecificGen/GF2519_32.v b/src/SpecificGen/GF2519_32.v
index b7fd074ae..98338b64c 100644
--- a/src/SpecificGen/GF2519_32.v
+++ b/src/SpecificGen/GF2519_32.v
@@ -176,6 +176,25 @@ Proof.
   etransitivity; apply app_n_correct.
 Qed.
 
+Definition appify9 {T} (op : 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 : 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' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+    @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+  intros. cbv [appify9].
+  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
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
 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))))))))).
+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
+               => 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 add_sig (f g : fe2519_32) :
   { fg : fe2519_32 | fg = add_opt f g}.
 Proof.
diff --git a/src/SpecificGen/GF25519_32.v b/src/SpecificGen/GF25519_32.v
index 30d01f87d..89f63a572 100644
--- a/src/SpecificGen/GF25519_32.v
+++ b/src/SpecificGen/GF25519_32.v
@@ -176,6 +176,25 @@ Proof.
   etransitivity; apply app_n_correct.
 Qed.
 
+Definition appify9 {T} (op : 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 : 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' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+    @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+  intros. cbv [appify9].
+  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
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
 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))))))))).
+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
+               => 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 add_sig (f g : fe25519_32) :
   { fg : fe25519_32 | fg = add_opt f g}.
 Proof.
diff --git a/src/SpecificGen/GF25519_64.v b/src/SpecificGen/GF25519_64.v
index 49b5fb2c4..3645a59f7 100644
--- a/src/SpecificGen/GF25519_64.v
+++ b/src/SpecificGen/GF25519_64.v
@@ -176,6 +176,25 @@ Proof.
   etransitivity; apply app_n_correct.
 Qed.
 
+Definition appify9 {T} (op : 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 : 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' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+    @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+  intros. cbv [appify9].
+  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
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
 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))))))))).
+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
+               => 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 add_sig (f g : fe25519_64) :
   { fg : fe25519_64 | fg = add_opt f g}.
 Proof.
diff --git a/src/SpecificGen/GF41417_32.v b/src/SpecificGen/GF41417_32.v
index 04ad4c173..9d0e73245 100644
--- a/src/SpecificGen/GF41417_32.v
+++ b/src/SpecificGen/GF41417_32.v
@@ -176,6 +176,25 @@ Proof.
   etransitivity; apply app_n_correct.
 Qed.
 
+Definition appify9 {T} (op : 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 : 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' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+    @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+  intros. cbv [appify9].
+  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
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
 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))))))))).
+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
+               => 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 add_sig (f g : fe41417_32) :
   { fg : fe41417_32 | fg = add_opt f g}.
 Proof.
diff --git a/src/SpecificGen/GF5211_32.v b/src/SpecificGen/GF5211_32.v
index ea75b2983..48f85104a 100644
--- a/src/SpecificGen/GF5211_32.v
+++ b/src/SpecificGen/GF5211_32.v
@@ -176,6 +176,25 @@ Proof.
   etransitivity; apply app_n_correct.
 Qed.
 
+Definition appify9 {T} (op : 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 : 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' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+    @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+  intros. cbv [appify9].
+  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
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
 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))))))))).
+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
+               => 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 add_sig (f g : fe5211_32) :
   { fg : fe5211_32 | fg = add_opt f g}.
 Proof.
diff --git a/src/SpecificGen/GFtemplate3mod4 b/src/SpecificGen/GFtemplate3mod4
index d255befeb..bc7766f7a 100644
--- a/src/SpecificGen/GFtemplate3mod4
+++ b/src/SpecificGen/GFtemplate3mod4
@@ -176,6 +176,25 @@ Proof.
   etransitivity; apply app_n_correct.
 Qed.
 
+Definition appify9 {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) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : 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' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+    @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+  intros. cbv [appify9].
+  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
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
 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))))))))).
+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
+               => 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 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 008010efd..7a0f0f22c 100644
--- a/src/SpecificGen/GFtemplate5mod8
+++ b/src/SpecificGen/GFtemplate5mod8
@@ -176,6 +176,25 @@ Proof.
   etransitivity; apply app_n_correct.
 Qed.
 
+Definition appify9 {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) (x0 x1 x2 x3 x4 x5 x6 x7 x8 : 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' =>
+                     op x0' x1' x2' x3' x4' x5' x6' x7' x8'))))))))).
+
+Lemma appify9_correct : forall {T} op x0 x1 x2 x3 x4 x5 x6 x7 x8,
+    @appify9 T op x0 x1 x2 x3 x4 x5 x6 x7 x8 = op x0 x1 x2 x3 x4 x5 x6 x7 x8.
+Proof.
+  intros. cbv [appify9].
+  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
@@ -190,6 +209,23 @@ Definition uncurry_unop_wire_digits {T} (op : wire_digits -> T)
 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))))))))).
+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
+               => 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 add_sig (f g : fe{{{k}}}{{{c}}}_{{{w}}}) :
   { fg : fe{{{k}}}{{{c}}}_{{{w}}} | fg = add_opt f g}.
 Proof.