Update AddCoordinates

Now the _correct_and_bounded lemma goes through

1 files changed, 17 insertions, 0 deletions

diff --git a/src/Util/Tower.v b/src/Util/Tower.v
index 6bcd44bf4..e3f57f3ed 100644
--- a/src/Util/Tower.v
+++ b/src/Util/Tower.v
@@ -1,5 +1,22 @@
 Require Export Crypto.Util.FixCoqMistakes.
 
+Definition apply4 {AK BK PA PB ARR}
+           (F : forall (A : AK) (B : BK), (PA A -> PB B) -> PB (ARR A B))
+           {A0 A1 A2 A3 : AK} {B : BK}
+           (f : PA A0 -> PA A1 -> PA A2 -> PA A3 -> PB B)
+  : PB (ARR A0 (ARR A1 (ARR A2 (ARR A3 B)))).
+Proof.
+  repeat (apply F; intro); apply f; assumption.
+Defined.
+
+Definition apply4_nd {BK PA PB ARR}
+           (F : forall (B : BK), (PA -> PB B) -> PB (ARR B))
+           {B : BK}
+           (f : PA -> PA -> PA -> PA -> PB B)
+  : PB (ARR (ARR (ARR (ARR B))))
+  := @apply4 unit BK (fun _ => PA) PB (fun _ => ARR) (fun _ => F)
+             tt tt tt tt B f.
+
 Definition apply9 {AK BK PA PB ARR}
            (F : forall (A : AK) (B : BK), (PA A -> PB B) -> PB (ARR A B))
            {A0 A1 A2 A3 A4 A5 A6 A7 A8 : AK} {B : BK}