3 files changed, 24 insertions, 3 deletions
diff --git a/src/Assembly/Pseudize.v b/src/Assembly/Pseudize.v
index af311963d..3a66484ee 100644
--- a/src/Assembly/Pseudize.v
+++ b/src/Assembly/Pseudize.v
@@ -162,6 +162,28 @@ Module Conversion.
     rewrite H0; autounfold; simpl; intuition.
   Qed.
 
+  Lemma pseudo_let_var:
+    forall {w s n k m} (p0: @Pseudo w s n k) (p1: @Pseudo w s (n + k) m)
+      input out0 out1 m0 m1 m2 c0 c1 c2,
+      pseudoEval p0 (input, m0, c0) = Some ([a], m1, c1)
+    -> pseudoEval p1 (input ++ [a], m1, c1) = Some (f (nth n (input ++ [a]) (wzero _)), m2, c2)
+    -> pseudoEval (@PLet w s n k m p0 p1) (input, m0, c0) =
+        Some (let x := a in f a, m2, c2).
+  Proof.
+    intros; cbv beta; simpl in *; apply pseudo_let.
+  Qed.
+
+  Lemma pseudo_let_list:
+    forall {w s n k m} (p0: @Pseudo w s n k) (p1: @Pseudo w s (n + k) m)
+      input out0 out1 m0 m1 m2 c0 c1 c2,
+      pseudoEval p0 (input, m0, c0) = Some (lst, m1, c1)
+    -> pseudoEval p1 (input ++ lst, m1, c1) = Some (f lst, m2, c2)
+    -> pseudoEval (@PLet w s n k m p0 p1) (input, m0, c0) =
+        Some (let x := lst in f a, m2, c2).
+  Proof.
+    intros; cbv beta; simpl in *; apply pseudo_let.
+  Qed.
+
   Definition pseudeq {w s} (n m: nat) (f: list (word w) -> list (word w)) : Type := 
     {p: @Pseudo w s n m | forall x: (list (word w)),
       List.length x = n -> exists m' c',
diff --git a/src/Assembly/QhasmUtil.v b/src/Assembly/QhasmUtil.v
index 078cf7780..f49d48573 100644
--- a/src/Assembly/QhasmUtil.v
+++ b/src/Assembly/QhasmUtil.v
@@ -1,4 +1,3 @@
-
 Require Import ZArith NArith NPeano.
 Require Import QhasmCommon.
 Require Export Bedrock.Word.
diff --git a/src/Spec/EdDSA.v b/src/Spec/EdDSA.v
index d71f2ad44..1e3e36ff9 100644
--- a/src/Spec/EdDSA.v
+++ b/src/Spec/EdDSA.v
@@ -4,8 +4,8 @@ Require Coq.ZArith.Znumtheory Coq.ZArith.BinInt.
 Require Coq.Numbers.Natural.Peano.NPeano.
 Require Crypto.CompleteEdwardsCurve.CompleteEdwardsCurveTheorems.
 
-Local Infix "^" := NPeano.pow.
-Local Infix "mod" := NPeano.modulo (at level 40, no associativity).
+Local Infix "^" := Nat.pow.
+Local Infix "mod" := Nat.modulo (at level 40, no associativity).
 Local Infix "++" := Word.combine.
 
 Generalizable All Variables.