1 files changed, 3 insertions, 4 deletions
diff --git a/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v b/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v
index d8d55ca04..49a4782eb 100644
--- a/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v
+++ b/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v
@@ -3,7 +3,6 @@ Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Application.
-Require Import Crypto.Reflection.MapInterp.
 Require Import Crypto.Util.Tactics.
 
 Local Opaque Interp.
@@ -42,7 +41,7 @@ Lemma Expr9_4Op_correct_and_bounded
           let (Hx7, Hx8) := (eta_and Hx78) in
           let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) (MapInterp BoundedWordW.of_wordW ropW))
+                  (ApplyInterpedAll (Interp (@BoundedWordW.interp_op) ropW)
                                     (LiftOption.to' (Some args)))
           with
           | Some _ => True
@@ -80,12 +79,12 @@ Lemma Expr9_4Op_correct_and_bounded
           let args := op9_args_to_bounded x012345678 Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8 in
           let x' := SmartVarfMap (fun _ : base_type => BoundedWordW.BoundedWordToBounds) args in
           match LiftOption.of'
-                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp ZBounds.of_wordW ropW)) (LiftOption.to' (Some x')))
+                  (ApplyInterpedAll (Interp (@ZBounds.interp_op) ropW) (LiftOption.to' (Some x')))
           with
           | Some bounds => op9_4_bounds_good bounds = true
           | None => False
           end)
-  : op9_4_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+  : op9_4_correct_and_bounded ropW op.
 Proof.
   intros x0 x1 x2 x3 x4 x5 x6 x7 x8.
   intros Hx0 Hx1 Hx2 Hx3 Hx4 Hx5 Hx6 Hx7 Hx8.