Remove the Const constructor of exprf

We instead use the [Op] constructor for constants.  This allows [exprf]
to not depend on the interpretation function; this means we don't need
to map over it to change the interpretation function.  This saves us
about 300 lines of code and about 30s of build time, total.

After     | File Name                                                              | Before    || Change
-----------------------------------------------------------------------------------------------------------
18m11.34s | Total                                                                  | 18m46.86s || -0m35.52s
-----------------------------------------------------------------------------------------------------------
0m19.99s  | Specific/GF25519ReflectiveAddCoordinates                               | 0m31.78s  || -0m11.79s
1m53.69s  | Specific/GF25519Reflective/Reified/LadderStep                          | 2m01.32s  || -0m07.62s
1m27.74s  | Specific/GF25519Reflective/Reified/AddCoordinates                      | 1m34.03s  || -0m06.29s
0m01.45s  | Specific/GF25519Reflective                                             | 0m06.31s  || -0m04.85s
0m04.62s  | Reflection/InlineInterp                                                | 0m01.52s  || +0m03.10s
1m19.68s  | CompleteEdwardsCurve/ExtendedCoordinates                               | 1m21.19s  || -0m01.50s
0m02.90s  | Reflection/InlineWf                                                    | 0m01.80s  || +0m01.09s
   N/A    | Reflection/MapWithInterpInfo                                           | 0m01.70s  || -0m01.70s
1m32.32s  | Test/Curve25519SpecTestVectors                                         | 1m32.25s  || +0m00.06s
1m12.79s  | Experiments/Ed25519                                                    | 1m13.17s  || -0m00.38s
0m40.52s  | ModularArithmetic/Conversion                                           | 0m40.44s  || +0m00.08s
0m34.57s  | Spec/Ed25519                                                           | 0m34.53s  || +0m00.03s
0m30.82s  | ModularArithmetic/ModularBaseSystemProofs                              | 0m30.89s  || -0m00.07s
0m30.11s  | Specific/GF25519Bounded                                                | 0m30.21s  || -0m00.10s
0m23.20s  | Experiments/MontgomeryCurve                                            | 0m23.26s  || -0m00.06s
0m22.16s  | Reflection/Z/Interpretations128/Relations                              | 0m21.72s  || +0m00.44s
0m21.69s  | ModularArithmetic/Pow2BaseProofs                                       | 0m21.58s  || +0m00.11s
0m20.25s  | Algebra                                                                | 0m20.27s  || -0m00.01s
0m19.81s  | Specific/GF25519                                                       | 0m19.83s  || -0m00.01s
0m18.82s  | Reflection/Z/Interpretations64/Relations                               | 0m18.50s  || +0m00.32s
0m18.19s  | EdDSARepChange                                                         | 0m18.26s  || -0m00.07s
0m17.08s  | CompleteEdwardsCurve/CompleteEdwardsCurveTheorems                      | 0m17.16s  || -0m00.08s
0m14.10s  | Util/ZUtil                                                             | 0m14.03s  || +0m00.07s
0m10.05s  | Testbit                                                                | 0m10.02s  || +0m00.03s
0m08.95s  | Specific/GF25519BoundedCommon                                          | 0m08.90s  || +0m00.04s
0m08.87s  | BoundedArithmetic/ArchitectureToZLikeProofs                            | 0m08.81s  || +0m00.05s
0m08.80s  | Assembly/GF25519                                                       | 0m08.82s  || -0m00.01s
0m08.80s  | ModularArithmetic/Montgomery/ZProofs                                   | 0m08.87s  || -0m00.06s
0m08.51s  | Encoding/PointEncoding                                                 | 0m08.53s  || -0m00.01s
0m08.37s  | BoundedArithmetic/Double/Proofs/Multiply                               | 0m08.39s  || -0m00.02s
0m08.34s  | Specific/GF1305                                                        | 0m08.31s  || +0m00.02s
0m07.85s  | BoundedArithmetic/Double/Proofs/ShiftRightDoubleWordImmediate          | 0m07.86s  || -0m00.01s
0m07.60s  | Specific/GF25519Reflective/Reified/Mul                                 | 0m07.52s  || +0m00.08s
0m07.13s  | MxDHRepChange                                                          | 0m07.08s  || +0m00.04s
0m06.85s  | BoundedArithmetic/Double/Proofs/SpreadLeftImmediate                    | 0m06.77s  || +0m00.08s
0m06.62s  | Reflection/Z/InterpretationsGen                                        | 0m06.62s  || +0m00.00s
0m05.69s  | Reflection/Z/Interpretations64/RelationsCombinations                   | 0m05.60s  || +0m00.09s
0m05.68s  | Reflection/Z/Interpretations128/RelationsCombinations                  | 0m05.67s  || +0m00.00s
0m05.48s  | Specific/SC25519                                                       | 0m05.38s  || +0m00.10s
0m05.40s  | BoundedArithmetic/Double/Proofs/RippleCarryAddSub                      | 0m05.36s  || +0m00.04s
0m04.93s  | ModularArithmetic/ModularBaseSystemListProofs                          | 0m04.96s  || -0m00.03s
0m04.87s  | WeierstrassCurve/Pre                                                   | 0m04.83s  || +0m00.04s
0m04.45s  | Specific/GF25519Reflective/Reified/PreFreeze                           | 0m04.56s  || -0m00.10s
0m04.33s  | Specific/GF25519Reflective/CommonBinOp                                 | 0m04.55s  || -0m00.21s
0m03.95s  | ModularArithmetic/BarrettReduction/ZHandbook                           | 0m03.98s  || -0m00.02s
0m03.87s  | Specific/GF25519Reflective/CommonUnOp                                  | 0m04.08s  || -0m00.20s
0m03.86s  | Encoding/PointEncodingPre                                              | 0m03.88s  || -0m00.02s
0m03.84s  | BaseSystemProofs                                                       | 0m03.88s  || -0m00.04s
0m03.75s  | Specific/GF25519Reflective/CommonUnOpWireToFE                          | 0m03.96s  || -0m00.20s
0m03.64s  | CompleteEdwardsCurve/Pre                                               | 0m03.60s  || +0m00.04s
0m03.51s  | BoundedArithmetic/InterfaceProofs                                      | 0m03.42s  || +0m00.08s
0m03.41s  | ModularArithmetic/Tutorial                                             | 0m03.38s  || +0m00.03s
0m03.30s  | Reflection/LinearizeWf                                                 | 0m04.24s  || -0m00.94s
0m03.20s  | Specific/GF25519Reflective/Reified/CarrySub                            | 0m03.28s  || -0m00.07s
0m03.14s  | ModularArithmetic/ZBoundedZ                                            | 0m03.14s  || +0m00.00s
0m03.14s  | ModularArithmetic/BarrettReduction/ZGeneralized                        | 0m03.14s  || +0m00.00s
0m02.95s  | Specific/GF25519Reflective/Reified/CarryAdd                            | 0m02.93s  || +0m00.02s
0m02.92s  | Specific/GF25519Reflective/Common9_4Op                                 | 0m02.89s  || +0m00.02s
0m02.82s  | Specific/GF25519Reflective/Reified/CarryOpp                            | 0m02.95s  || -0m00.13s
0m02.82s  | BoundedArithmetic/Double/Proofs/Decode                                 | 0m02.90s  || -0m00.08s
0m02.69s  | BoundedArithmetic/Double/Proofs/ShiftRight                             | 0m02.69s  || +0m00.00s
0m02.66s  | ModularArithmetic/ModularArithmeticTheorems                            | 0m02.67s  || -0m00.00s
0m02.63s  | Specific/FancyMachine256/Montgomery                                    | 0m02.24s  || +0m00.38s
0m02.61s  | Specific/GF25519Reflective/CommonUnOpFEToWire                          | 0m02.76s  || -0m00.14s
0m02.58s  | BoundedArithmetic/Double/Proofs/ShiftLeft                              | 0m02.58s  || +0m00.00s
0m02.56s  | Specific/GF25519Reflective/Common                                      | 0m02.60s  || -0m00.04s
0m02.52s  | Specific/FancyMachine256/Barrett                                       | 0m02.20s  || +0m00.31s
0m02.50s  | Specific/GF25519BoundedAddCoordinates                                  | 0m02.60s  || -0m00.10s
0m02.39s  | ModularArithmetic/BarrettReduction/ZBounded                            | 0m02.31s  || +0m00.08s
0m02.34s  | ModularArithmetic/ModularBaseSystemOpt                                 | 0m02.31s  || +0m00.02s
0m02.02s  | Specific/GF25519Reflective/Reified/Sub                                 | 0m02.01s  || +0m00.01s
0m01.98s  | Reflection/WfReflective                                                | 0m02.54s  || -0m00.56s
0m01.94s  | Specific/GF25519Reflective/Reified/Pack                                | 0m02.07s  || -0m00.12s
0m01.93s  | Assembly/Evaluables                                                    | 0m01.93s  || +0m00.00s
0m01.92s  | Specific/GF25519Reflective/Reified/Unpack                              | 0m02.04s  || -0m00.12s
0m01.90s  | Specific/FancyMachine256/Core                                          | 0m01.79s  || +0m00.10s
0m01.79s  | ModularArithmetic/Montgomery/ZBounded                                  | 0m01.86s  || -0m00.07s
0m01.77s  | Specific/GF25519ExtendedAddCoordinates                                 | 0m01.76s  || +0m00.01s
0m01.68s  | Specific/GF25519Reflective/Reified/Add                                 | 0m01.69s  || -0m00.01s
0m01.67s  | Specific/GF25519BoundedExtendedAddCoordinates                          | 0m01.79s  || -0m00.12s
0m01.63s  | Experiments/Ed25519Extraction                                          | 0m01.66s  || -0m00.03s
0m01.62s  | Specific/GF25519Reflective/Reified/Opp                                 | 0m01.72s  || -0m00.09s
0m01.54s  | Specific/GF25519Reflective/Reified/GeModulus                           | 0m01.59s  || -0m00.05s
0m01.50s  | Reflection/TestCase                                                    | 0m01.42s  || +0m00.08s
0m01.47s  | ModularArithmetic/BarrettReduction/Z                                   | 0m01.47s  || +0m00.00s
0m01.43s  | Assembly/Compile                                                       | 0m01.46s  || -0m00.03s
0m01.33s  | Reflection/WfProofs                                                    | 0m01.95s  || -0m00.61s
0m01.26s  | ModularArithmetic/PrimeFieldTheorems                                   | 0m01.28s  || -0m00.02s
0m01.20s  | Assembly/Conversions                                                   | 0m01.19s  || +0m00.01s
0m01.16s  | ModularArithmetic/ExtendedBaseVector                                   | 0m01.22s  || -0m00.06s
0m01.16s  | BaseSystem                                                             | 0m01.15s  || +0m00.01s
0m01.09s  | BoundedArithmetic/Double/Repeated/Proofs/Decode                        | 0m01.11s  || -0m00.02s
0m00.99s  | Util/NumTheoryUtil                                                     | 0m00.96s  || +0m00.03s
0m00.96s  | Assembly/HL                                                            | 0m00.96s  || +0m00.00s
0m00.94s  | Assembly/LL                                                            | 0m00.99s  || -0m00.05s
0m00.94s  | Assembly/Pipeline                                                      | 0m00.92s  || +0m00.01s
0m00.88s  | Reflection/WfInversion                                                 | 0m01.21s  || -0m00.32s
0m00.86s  | Assembly/PhoasCommon                                                   | 0m00.91s  || -0m00.05s
0m00.86s  | Specific/GF25519Reflective/CommonUnOpFEToZ                             | 0m01.02s  || -0m00.16s
0m00.85s  | BoundedArithmetic/Double/Proofs/LoadImmediate                          | 0m00.86s  || -0m00.01s
0m00.84s  | BoundedArithmetic/Double/Proofs/BitwiseOr                              | 0m00.91s  || -0m00.07s
0m00.82s  | BoundedArithmetic/X86ToZLikeProofs                                     | 0m00.85s  || -0m00.03s
0m00.79s  | Util/IterAssocOp                                                       | 0m00.82s  || -0m00.02s
0m00.75s  | Reflection/Z/Syntax                                                    | 0m00.67s  || +0m00.07s
0m00.73s  | Util/PartiallyReifiedProp                                              | 0m00.73s  || +0m00.00s
0m00.70s  | Encoding/ModularWordEncodingTheorems                                   | 0m00.76s  || -0m00.06s
0m00.70s  | Specific/GF25519Reflective/Reified                                     | 0m00.72s  || -0m00.02s
0m00.66s  | BoundedArithmetic/Double/Repeated/Proofs/Multiply                      | 0m00.62s  || +0m00.04s
0m00.66s  | ModularArithmetic/PseudoMersenneBaseParamProofs                        | 0m00.66s  || +0m00.00s
0m00.64s  | Encoding/ModularWordEncodingPre                                        | 0m00.63s  || +0m00.01s
0m00.61s  | ModularArithmetic/ModularBaseSystem                                    | 0m00.66s  || -0m00.05s
0m00.61s  | Util/AdditionChainExponentiation                                       | 0m00.64s  || -0m00.03s
0m00.60s  | ModularArithmetic/ExtPow2BaseMulProofs                                 | 0m00.64s  || -0m00.04s
0m00.60s  | Reflection/MultiSizeTest2                                              | 0m00.71s  || -0m00.10s
0m00.60s  | Spec/EdDSA                                                             | 0m00.65s  || -0m00.05s
0m00.59s  | BoundedArithmetic/Double/Repeated/Proofs/RippleCarryAddSub             | 0m00.51s  || +0m00.07s
0m00.58s  | BoundedArithmetic/Interface                                            | 0m00.60s  || -0m00.02s
0m00.58s  | ModularArithmetic/ModularBaseSystemList                                | 0m00.61s  || -0m00.03s
0m00.55s  | Spec/ModularWordEncoding                                               | 0m00.63s  || -0m00.07s
0m00.55s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftLeftRight                | 0m00.50s  || +0m00.05s
0m00.55s  | Reflection/InterpWfRel                                                 | 0m00.58s  || -0m00.02s
0m00.54s  | BoundedArithmetic/X86ToZLike                                           | 0m00.55s  || -0m00.01s
0m00.54s  | BoundedArithmetic/Double/Repeated/Proofs/SelectConditional             | 0m00.53s  || +0m00.01s
0m00.54s  | BoundedArithmetic/Double/Proofs/SelectConditional                      | 0m00.62s  || -0m00.07s
0m00.54s  | Reflection/WfReflectiveGen                                             | 0m00.58s  || -0m00.03s
0m00.52s  | BoundedArithmetic/ArchitectureToZLike                                  | 0m00.41s  || +0m00.11s
0m00.51s  | BoundedArithmetic/Double/Core                                          | 0m00.48s  || +0m00.03s
0m00.50s  | BoundedArithmetic/Double/Repeated/Proofs/BitwiseOr                     | 0m00.51s  || -0m00.01s
0m00.49s  | Spec/WeierstrassCurve                                                  | 0m00.42s  || +0m00.07s
0m00.48s  | BoundedArithmetic/Double/Repeated/Proofs/LoadImmediate                 | 0m00.54s  || -0m00.06s
0m00.47s  | BoundedArithmetic/Double/Repeated/Proofs/ShiftRightDoubleWordImmediate | 0m00.58s  || -0m00.10s
0m00.47s  | Reflection/InterpWf                                                    | 0m00.50s  || -0m00.03s
0m00.47s  | ModularArithmetic/Pre                                                  | 0m00.48s  || -0m00.01s
0m00.47s  | BoundedArithmetic/Double/Repeated/Core                                 | 0m00.46s  || +0m00.00s
0m00.46s  | Reflection/Z/Interpretations64                                         | 0m00.49s  || -0m00.02s
0m00.45s  | Reflection/InputSyntax                                                 | 0m00.42s  || +0m00.03s
   N/A    | Reflection/MapInterpWf                                                 | 0m00.44s  || -0m00.44s
0m00.44s  | Spec/CompleteEdwardsCurve                                              | 0m00.39s  || +0m00.04s
0m00.44s  | BoundedArithmetic/Double/Proofs/ShiftLeftRightTactic                   | 0m00.42s  || +0m00.02s
0m00.44s  | Reflection/Z/Interpretations128                                        | 0m00.52s  || -0m00.08s
0m00.44s  | ModularArithmetic/ZBounded                                             | 0m00.45s  || -0m00.01s
0m00.42s  | BoundedArithmetic/StripCF                                              | 0m00.42s  || +0m00.00s
0m00.42s  | Reflection/Z/Reify                                                     | 0m00.43s  || -0m00.01s
0m00.42s  | ModularArithmetic/ModularBaseSystemListZOperationsProofs               | 0m00.47s  || -0m00.04s
0m00.41s  | Reflection/Named/DeadCodeElimination                                   | 0m00.43s  || -0m00.02s
0m00.41s  | ModularArithmetic/PseudoMersenneBaseParams                             | 0m00.38s  || +0m00.02s
0m00.41s  | Spec/ModularArithmetic                                                 | 0m00.34s  || +0m00.06s
0m00.41s  | Reflection/Named/RegisterAssign                                        | 0m00.37s  || +0m00.03s
0m00.41s  | Reflection/Reify                                                       | 0m00.39s  || +0m00.01s
0m00.40s  | ModularArithmetic/Pow2Base                                             | 0m00.42s  || -0m00.01s
0m00.40s  | Reflection/Named/EstablishLiveness                                     | 0m00.33s  || +0m00.07s
0m00.40s  | Reflection/ExprInversion                                               | 0m00.57s  || -0m00.16s
0m00.40s  | Reflection/Named/Syntax                                                | 0m00.40s  || +0m00.00s
0m00.38s  | Reflection/Named/Compile                                               | 0m00.34s  || +0m00.03s
   N/A    | Reflection/MapInterp                                                   | 0m00.38s  || -0m00.38s
0m00.38s  | ModularArithmetic/Montgomery/Z                                         | 0m00.39s  || -0m00.01s
0m00.38s  | ModularArithmetic/ModularBaseSystemWord                                | 0m00.36s  || +0m00.02s
   N/A    | Reflection/WfRel                                                       | 0m00.38s  || -0m00.38s
0m00.38s  | Reflection/Tuple                                                       |    N/A    || +0m00.38s
0m00.37s  | Spec/MxDH                                                              | 0m00.39s  || -0m00.02s
0m00.37s  | BoundedArithmetic/Eta                                                  | 0m00.36s  || +0m00.01s
0m00.36s  | Reflection/Named/ContextOn                                             | 0m00.37s  || -0m00.01s
0m00.34s  | Reflection/FilterLive                                                  | 0m00.34s  || +0m00.00s
0m00.34s  | Reflection/LinearizeInterp                                             | 0m00.53s  || -0m00.19s
0m00.33s  | Reflection/Relations                                                   |    N/A    || +0m00.33s
0m00.32s  | Reflection/Equality                                                    | 0m00.41s  || -0m00.08s
0m00.30s  | Reflection/Syntax                                                      | 0m00.52s  || -0m00.22s
0m00.30s  | Reflection/InterpProofs                                                | 0m00.47s  || -0m00.17s
0m00.30s  | Reflection/ApplicationLemmas                                           | 0m00.43s  || -0m00.13s
0m00.30s  | Reflection/CommonSubexpressionElimination                              | 0m00.50s  || -0m00.20s
0m00.28s  | Reflection/Inline                                                      | 0m00.37s  || -0m00.08s
0m00.28s  | Reflection/Conversion                                                  | 0m00.44s  || -0m00.15s
0m00.27s  | Reflection/MapCastWithCastOp                                           | 0m00.38s  || -0m00.10s
0m00.26s  | Reflection/MapCast                                                     | 0m00.40s  || -0m00.14s
0m00.26s  | Reflection/ApplicationRelations                                        | 0m00.35s  || -0m00.08s
0m00.24s  | Reflection/Application                                                 | 0m00.38s  || -0m00.14s
0m00.23s  | Reflection/Linearize                                                   | 0m00.35s  || -0m00.11s
0m00.20s  | Reflection/CountLets                                                   | 0m00.33s  || -0m00.13s
0m00.20s  | Reflection/Named/NameUtil                                              | 0m00.36s  || -0m00.15s
0m00.09s  | Util/PointedProp                                                       | 0m00.08s  || +0m00.00s
0m00.05s  | Util/LetIn                                                             | 0m00.06s  || -0m00.00s
0m00.03s  | Util/Notations                                                         | 0m00.03s  || +0m00.00s
0m00.03s  | Util/AutoRewrite                                                       | 0m00.03s  || +0m00.00s

14 files changed, 148 insertions, 167 deletions

diff --git a/src/Specific/FancyMachine256/Barrett.v b/src/Specific/FancyMachine256/Barrett.v
index f3258fe60..93a9432aa 100644
--- a/src/Specific/FancyMachine256/Barrett.v
+++ b/src/Specific/FancyMachine256/Barrett.v
@@ -63,7 +63,7 @@ End expression.
 
 Section reflected.
   Context (ops : fancy_machine.instructions (2 * 128)).
-  Definition rexpression : Syntax.Expr base_type (interp_base_type _) op (Arrow TZ (Arrow TZ (Arrow TW (Arrow TW (Tbase TW))))).
+  Definition rexpression : Syntax.Expr base_type op (Arrow TZ (Arrow TZ (Arrow TW (Arrow TW (Tbase TW))))).
   Proof.
     let v := (eval cbv beta delta [expression] in (fun m μ x y => expression ops m μ (x, y))) in
     let v := Reify v in
@@ -85,7 +85,7 @@ Section reflected.
   Context (m μ : Z)
           (props : fancy_machine.arithmetic ops).
 
-  Let result (v : Tuple.tuple fancy_machine.W 2) := Syntax.Interp (interp_op _) rexpression_simple m μ (fst v) (snd v).
+  Let result (v : Tuple.tuple fancy_machine.W 2) := Syntax.Interp interp_op rexpression_simple m μ (fst v) (snd v).
   Let assembled_result (v : Tuple.tuple fancy_machine.W 2) : fancy_machine.W := Core.Interp compiled_syntax m μ (fst v) (snd v).
 
   Theorem sanity : result = expression ops m μ.
@@ -148,12 +148,5 @@ c.Sub(tmp, x, tmp),
 c.Addm(q, tmp, RegZero),
 c.Addm(out, q, RegZero),
 Return out
-     : forall ops : fancy_machine.instructions (2 * 128),
-       expr base_type
-         (fun v : base_type =>
-          match v with
-          | TZ => Z
-          | Tbool => bool
-          | TW => let (W, _, _, _, _, _, _, _, _, _, _, _, _, _) := ops in W
-          end) op Register (TZ -> TZ -> TW -> TW -> Tbase TW)%ctype
+     : forall ops : fancy_machine.instructions (2 * 128), expr base_type op Register (TZ -> TZ -> TW -> TW -> Tbase TW)
 *)
diff --git a/src/Specific/FancyMachine256/Core.v b/src/Specific/FancyMachine256/Core.v
index eb443a8e3..9dd66e777 100644
--- a/src/Specific/FancyMachine256/Core.v
+++ b/src/Specific/FancyMachine256/Core.v
@@ -30,7 +30,7 @@ Local Notation eta3' x := (fst x, eta (snd x)).
 
 (** ** Reflective Assembly Syntax *)
 Section reflection.
-  Context (ops : fancy_machine.instructions (2 * 128)).
+  Context {ops : fancy_machine.instructions (2 * 128)}.
   Local Set Boolean Equality Schemes.
   Local Set Decidable Equality Schemes.
   Inductive base_type := TZ | Tbool | TW.
@@ -47,6 +47,7 @@ Section reflection.
   Local Notation tW := (Tbase TW).
   Local Open Scope ctype_scope.
   Inductive op : flat_type base_type -> flat_type base_type -> Type :=
+  | OPconst t : interp_base_type t -> op Unit (Tbase t)
   | OPldi     : op tZ tW
   | OPshrd    : op (tW * tW * tZ) tW
   | OPshl     : op (tW * tZ) tW
@@ -59,9 +60,13 @@ Section reflection.
   | OPselc    : op (tbool * tW * tW) tW
   | OPaddm    : op (tW * tW * tW) tW.
 
+  Definition is_const s d (v : op s d) : bool
+    := match v with OPconst _ _ => true | _ => false end.
+
   Definition interp_op src dst (f : op src dst)
     : interp_flat_type interp_base_type src -> interp_flat_type interp_base_type dst
     := match f in op s d return interp_flat_type _ s -> interp_flat_type _ d with
+       | OPconst _ v => fun _ => v
        | OPldi     => ldi
        | OPshrd    => fun xyz => let '(x, y, z) := eta3 xyz in shrd x y z
        | OPshl     => fun xy => let '(x, y) := eta xy in shl x y
@@ -75,19 +80,16 @@ Section reflection.
        | OPaddm    => fun xyz => let '(x, y, z) := eta3 xyz in addm x y z
        end.
 
-  Inductive SConstT := ZConst (_ : Z) | BoolConst (_ : bool) | INVALID_CONST.
-  Inductive op_code : Set :=
+  Inductive op_code : Type :=
+  | SOPconstb (v : bool) | SOPconstZ (v : Z) | SOPconstW
   | SOPldi | SOPshrd | SOPshl | SOPshr | SOPadc | SOPsubc
   | SOPmulhwll | SOPmulhwhl | SOPmulhwhh | SOPselc | SOPaddm.
 
-  Definition symbolicify_const (t : base_type) : interp_base_type t -> SConstT
-    := match t with
-       | TZ => fun x => ZConst x
-       | Tbool => fun x => BoolConst x
-       | TW => fun x => INVALID_CONST
-       end.
   Definition symbolicify_op s d (v : op s d) : op_code
     := match v with
+       | OPconst TZ v => SOPconstZ v
+       | OPconst Tbool v => SOPconstb v
+       | OPconst TW v => SOPconstW
        | OPldi => SOPldi
        | OPshrd => SOPshrd
        | OPshl => SOPshl
@@ -101,28 +103,29 @@ Section reflection.
        | OPaddm => SOPaddm
        end.
 
-  Definition CSE {t} e := @CSE base_type SConstT op_code base_type_beq SConstT_beq op_code_beq internal_base_type_dec_bl interp_base_type op symbolicify_const symbolicify_op t e (fun _ => nil).
+  Definition CSE {t} e := @CSE base_type op_code base_type_beq op_code_beq internal_base_type_dec_bl op symbolicify_op t e (fun _ => nil).
 
   Inductive inline_option := opt_inline | opt_default | opt_noinline.
 
-  Definition postprocess var t (e : @exprf base_type interp_base_type op var t)
-    : @inline_directive base_type interp_base_type op var t
+  Definition postprocess var t (e : @exprf base_type op var t)
+    : @inline_directive base_type op var t
     := let opt : inline_option
            := match e with
               | Op _ _ OPshl _ => opt_inline
               | Op _ _ OPshr _ => opt_inline
+              | Op _ _ (OPconst _ _) _ => opt_inline
               | _ => opt_default
               end in
        match opt with
        | opt_noinline => no_inline e
        | opt_default => default_inline e
-       | opt_inline => match t as t' return exprf _ _ _ t' -> inline_directive t' with
+       | opt_inline => match t as t' return exprf _ _ t' -> inline_directive t' with
                        | Tbase _ => fun e => inline e
                        | _ => fun e => default_inline e
                        end e
        end.
 
-  Definition Inline {t} e := @InlineConstGen base_type interp_base_type op postprocess t e.
+  Definition Inline {t} e := @InlineConstGen base_type op postprocess t e.
 End reflection.
 
 Ltac base_reify_op op op_head expr ::=
@@ -146,10 +149,10 @@ Ltac base_reify_type T ::=
      | fancy_machine.W => TW
      end.
 
-Ltac Reify' e := Reify.Reify' base_type (interp_base_type _) op e.
+Ltac Reify' e := Reify.Reify' base_type (@interp_base_type _) (@op _) e.
 Ltac Reify e :=
-  let v := Reify.Reify base_type (interp_base_type _) op e in
-  constr:(Inline _ ((*CSE _*) (InlineConst (Linearize v)))).
+  let v := Reify.Reify base_type (@interp_base_type _) (@op _) (@OPconst _) e in
+  constr:(Inline ((*CSE _*) (InlineConst (@is_const _) (Linearize v)))).
 (*Ltac Reify_rhs := Reify.Reify_rhs base_type (interp_base_type _) op (interp_op _).*)
 
 (** ** Raw Syntax Trees *)
@@ -207,10 +210,10 @@ Global Instance RegisterContext {var : base_type -> Type} : Context Register var
   := ContextOn pos_of_Register (RegisterAssign.pos_context var).
 
 Definition syntax {ops : fancy_machine.instructions (2 * 128)}
-  := Named.expr base_type (interp_base_type ops) op Register.
+  := Named.expr base_type op Register.
 
-Class wf_empty {ops} {var} {t} (e : Named.expr base_type (interp_base_type ops) op Register t)
-  := mk_wf_empty : @Named.wf base_type (interp_base_type ops) op Register var _ empty t e.
+Class wf_empty {ops} {var} {t} (e : Named.expr base_type (@op ops) Register t)
+  := mk_wf_empty : @Named.wf base_type op Register var _ empty t e.
 Global Hint Extern 0 (wf_empty _) => vm_compute; intros; constructor : typeclass_instances.
 
 (** Assemble a well-typed easily interpretable expression into a
@@ -218,7 +221,7 @@ Global Hint Extern 0 (wf_empty _) => vm_compute; intros; constructor : typeclass
 Section assemble.
   Context {ops : fancy_machine.instructions (2 * 128)}.
 
-  Definition AssembleSyntax' {t} (e : Expr base_type (interp_base_type _) op t) (ls : list Register)
+  Definition AssembleSyntax' {t} (e : Expr base_type op t) (ls : list Register)
     : option (syntax t)
     := CompileAndEliminateDeadCode e ls.
   Definition AssembleSyntax {t} e ls (res := @AssembleSyntax' t e ls)
@@ -229,13 +232,13 @@ Section assemble.
 
   Definition dummy_registers (n : nat) : list Register
     := List.map scratchplus (seq 0 n).
-  Definition DefaultRegisters {t} (e : Expr base_type (interp_base_type _) op t) : list Register
+  Definition DefaultRegisters {t} (e : Expr base_type op t) : list Register
     := dummy_registers (CountBinders e).
 
   Definition DefaultAssembleSyntax {t} e := @AssembleSyntax t e (DefaultRegisters e).
 
   Definition Interp {t} e {wf : wf_empty e}
-    := @Named.interp base_type (interp_base_type _) op Register _ (interp_op _) empty t e wf.
+    := @Named.interp base_type interp_base_type op Register _ interp_op empty t e wf.
 End assemble.
 
 Export Reflection.Named.Syntax.
@@ -245,6 +248,7 @@ Open Scope type_scope.
 Open Scope core_scope.
 
 Notation Return x := (Var x).
+Notation Const z := (Op (@OPconst _ _ z) TT).
 Notation ldi z := (Op OPldi (Const z%Z)).
 Notation "'slet' x := A 'in' b" := (LetIn _ x (Op OPldi (Var A%nexpr)) b%nexpr) : nexpr_scope.
 Notation "'c.Rshi' ( x , A , B , C ) , b" :=
diff --git a/src/Specific/FancyMachine256/Montgomery.v b/src/Specific/FancyMachine256/Montgomery.v
index b6f2da64a..f0ca09119 100644
--- a/src/Specific/FancyMachine256/Montgomery.v
+++ b/src/Specific/FancyMachine256/Montgomery.v
@@ -53,7 +53,7 @@ End expression.
 
 Section reflected.
   Context (ops : fancy_machine.instructions (2 * 128)).
-  Definition rexpression : Syntax.Expr base_type (interp_base_type _) op (Arrow TZ (Arrow TZ (Arrow TW (Arrow TW (Tbase TW))))).
+  Definition rexpression : Syntax.Expr base_type op (Arrow TZ (Arrow TZ (Arrow TW (Arrow TW (Tbase TW))))).
   Proof.
     let v := (eval cbv beta delta [expression] in (fun modulus m' x y => expression ops modulus m' (x, y))) in
     let v := Reify v in
@@ -76,7 +76,7 @@ Section reflected.
   Context (modulus m' : Z)
           (props : fancy_machine.arithmetic ops).
 
-  Let result (v : Tuple.tuple fancy_machine.W 2) := Syntax.Interp (interp_op _) rexpression_simple modulus m' (fst v) (snd v).
+  Let result (v : Tuple.tuple fancy_machine.W 2) := Syntax.Interp interp_op rexpression_simple modulus m' (fst v) (snd v).
 
   Let assembled_result (v : Tuple.tuple fancy_machine.W 2) : fancy_machine.W := Core.Interp compiled_syntax modulus m' (fst v) (snd v).
 
@@ -147,12 +147,5 @@ c.Selc(y, RegMod, RegZero),
 c.Sub(lo, hi, y),
 c.Addm(lo, lo, RegZero),
 Return lo
-     : forall ops : fancy_machine.instructions (2 * 128),
-       expr base_type
-         (fun v : base_type =>
-          match v with
-          | TZ => Z
-          | Tbool => bool
-          | TW => let (W, _, _, _, _, _, _, _, _, _, _, _, _, _) := ops in W
-          end) op Register (TZ -> TZ -> TW -> TW -> Tbase TW)%ctype
+     : forall ops : fancy_machine.instructions (2 * 128), expr base_type op Register (TZ -> TZ -> TW -> TW -> Tbase TW)
 *)
diff --git a/src/Specific/GF25519Reflective.v b/src/Specific/GF25519Reflective.v
index b981747a1..dd4545094 100644
--- a/src/Specific/GF25519Reflective.v
+++ b/src/Specific/GF25519Reflective.v
@@ -9,7 +9,6 @@ Require Export Crypto.Specific.GF25519.
 Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.MapInterp.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
@@ -50,7 +49,7 @@ Declare Reduction asm_interp
             WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type WordW.interp_base_type word64ize
             Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd].
 Ltac asm_interp
   := cbv beta iota delta
@@ -61,41 +60,41 @@ Ltac asm_interp
             WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type WordW.interp_base_type word64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 
 
 Definition interp_radd : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
-  := Eval asm_interp in interp_bexpr (rword64ize radd).
+  := Eval asm_interp in interp_bexpr radd.
 (*Print interp_radd.*)
 Definition interp_radd_correct : interp_radd = interp_bexpr radd := eq_refl.
 Definition interp_rsub : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
-  := Eval asm_interp in interp_bexpr (rword64ize rsub).
+  := Eval asm_interp in interp_bexpr rsub.
 (*Print interp_rsub.*)
 Definition interp_rsub_correct : interp_rsub = interp_bexpr rsub := eq_refl.
 Definition interp_rmul : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
-  := Eval asm_interp in interp_bexpr (rword64ize rmul).
+  := Eval asm_interp in interp_bexpr rmul.
 (*Print interp_rmul.*)
 Definition interp_rmul_correct : interp_rmul = interp_bexpr rmul := eq_refl.
 Definition interp_ropp : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
-  := Eval asm_interp in interp_uexpr (rword64ize ropp).
+  := Eval asm_interp in interp_uexpr ropp.
 (*Print interp_ropp.*)
 Definition interp_ropp_correct : interp_ropp = interp_uexpr ropp := eq_refl.
 Definition interp_rprefreeze : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.fe25519W
-  := Eval asm_interp in interp_uexpr (rword64ize rprefreeze).
+  := Eval asm_interp in interp_uexpr rprefreeze.
 (*Print interp_rprefreeze.*)
 Definition interp_rprefreeze_correct : interp_rprefreeze = interp_uexpr rprefreeze := eq_refl.
 
 Definition interp_rge_modulus : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.word64
-  := Eval asm_interp in interp_uexpr_FEToZ (rword64ize rge_modulus).
+  := Eval asm_interp in interp_uexpr_FEToZ rge_modulus.
 Definition interp_rge_modulus_correct : interp_rge_modulus = interp_uexpr_FEToZ rge_modulus := eq_refl.
 
 Definition interp_rpack : Specific.GF25519BoundedCommon.fe25519W -> Specific.GF25519BoundedCommon.wire_digitsW
-  := Eval asm_interp in interp_uexpr_FEToWire (rword64ize rpack).
+  := Eval asm_interp in interp_uexpr_FEToWire rpack.
 Definition interp_rpack_correct : interp_rpack = interp_uexpr_FEToWire rpack := eq_refl.
 
 Definition interp_runpack : Specific.GF25519BoundedCommon.wire_digitsW -> Specific.GF25519BoundedCommon.fe25519W
-  := Eval asm_interp in interp_uexpr_WireToFE (rword64ize runpack).
+  := Eval asm_interp in interp_uexpr_WireToFE runpack.
 Definition interp_runpack_correct : interp_runpack = interp_uexpr_WireToFE runpack := eq_refl.
 
 Lemma radd_correct_and_bounded : binop_correct_and_bounded radd carry_add.
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index b65c852c0..d47e71933 100644
--- a/src/Specific/GF25519Reflective/Common.v
+++ b/src/Specific/GF25519Reflective/Common.v
@@ -4,6 +4,8 @@ Require Export Crypto.Specific.GF25519.
 Require Export Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.ExprInversion.
+Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
@@ -11,8 +13,6 @@ Require Import Crypto.Reflection.Z.Reify.
 Require Export Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.InterpWfRel.
 Require Import Crypto.Reflection.Application.
-Require Import Crypto.Reflection.MapInterp.
-Require Import Crypto.Reflection.MapInterpWf.
 Require Import Crypto.Reflection.WfReflective.
 Require Import Crypto.Util.Tower.
 Require Import Crypto.Util.LetIn.
@@ -21,7 +21,7 @@ Require Import Crypto.Util.ZUtil.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
 
-Notation Expr := (Expr base_type WordW.interp_base_type op).
+Notation Expr := (Expr base_type op).
 
 Local Ltac make_type_from' T :=
   let T := (eval compute in T) in
@@ -76,20 +76,20 @@ Definition ExprArg : Type := Expr ExprArgT.
 Definition ExprArgWire : Type := Expr ExprArgWireT.
 Definition ExprArgRev : Type := Expr ExprArgRevT.
 Definition ExprArgWireRev : Type := Expr ExprArgWireRevT.
-Definition expr_nm_Op count_in count_out interp_base_type var : Type
-  := expr base_type interp_base_type op (var:=var) (Expr_nm_OpT count_in count_out).
-Definition exprBinOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprBinOpT.
-Definition exprUnOp interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpT.
-Definition expr4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr4OpT.
-Definition expr9_4Op interp_base_type var : Type := expr base_type interp_base_type op (var:=var) Expr9_4OpT.
-Definition exprZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) (Tbase TZ).
-Definition exprUnOpFEToZ interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToZT.
-Definition exprUnOpWireToFE interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpWireToFET.
-Definition exprUnOpFEToWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprUnOpFEToWireT.
-Definition exprArg interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgT.
-Definition exprArgWire interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireT.
-Definition exprArgRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgRevT.
-Definition exprArgWireRev interp_base_type var : Type := expr base_type interp_base_type op (var:=var) ExprArgWireRevT.
+Definition expr_nm_Op count_in count_out var : Type
+  := expr base_type op (var:=var) (Expr_nm_OpT count_in count_out).
+Definition exprBinOp var : Type := expr base_type op (var:=var) ExprBinOpT.
+Definition exprUnOp var : Type := expr base_type op (var:=var) ExprUnOpT.
+Definition expr4Op var : Type := expr base_type op (var:=var) Expr4OpT.
+Definition expr9_4Op var : Type := expr base_type op (var:=var) Expr9_4OpT.
+Definition exprZ var : Type := expr base_type op (var:=var) (Tbase TZ).
+Definition exprUnOpFEToZ var : Type := expr base_type op (var:=var) ExprUnOpFEToZT.
+Definition exprUnOpWireToFE var : Type := expr base_type op (var:=var) ExprUnOpWireToFET.
+Definition exprUnOpFEToWire var : Type := expr base_type op (var:=var) ExprUnOpFEToWireT.
+Definition exprArg var : Type := expr base_type op (var:=var) ExprArgT.
+Definition exprArgWire var : Type := expr base_type op (var:=var) ExprArgWireT.
+Definition exprArgRev var : Type := expr base_type op (var:=var) ExprArgRevT.
+Definition exprArgWireRev var : Type := expr base_type op (var:=var) ExprArgWireRevT.
 
 Local Ltac bounds_from_list_cps ls :=
   lazymatch (eval hnf in ls) with
@@ -204,10 +204,10 @@ Notation rexpr_9_4op_sig op := (rexpr_sig Expr9_4OpT (uncurry_9op_fe25519 op)) (
 Notation correct_and_bounded_genT ropW'v ropZ_sigv
   := (let ropW' := ropW'v in
       let ropZ_sig := ropZ_sigv in
-      let ropW := MapInterp (fun _ x => x) ropW' in
-      let ropZ := MapInterp WordW.to_Z ropW' in
-      let ropBounds := MapInterp ZBounds.of_wordW ropW' in
-      let ropBoundedWordW := MapInterp BoundedWordW.of_wordW ropW' in
+      let ropW := ropW' in
+      let ropZ := ropW' in
+      let ropBounds := ropW' in
+      let ropBoundedWordW := ropW' in
       ropZ = proj1_sig ropZ_sig
       /\ interp_type_rel_pointwise2 Relations.related_Z (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@Z.interp_op) ropZ)
       /\ interp_type_rel_pointwise2 Relations.related_bounds (Interp (@BoundedWordW.interp_op) ropBoundedWordW) (Interp (@ZBounds.interp_op) ropBounds)
@@ -327,17 +327,17 @@ Ltac assoc_right_tuple x so_far :=
 Local Ltac make_args x :=
   let x' := fresh "x'" in
   compute in x |- *;
-  let t := match type of x with @expr _ _ _ _ (Tflat ?t) => t end in
-  let t' := match goal with |- @expr _ _ _ _ (Tflat ?t) => t end in
-  refine (LetIn (UnReturn x) _);
+  let t := match type of x with @expr _ _ _ (Tflat ?t) => t end in
+  let t' := match goal with |- @expr _ _ _ (Tflat ?t) => t end in
+  refine (LetIn (invert_Return x) _);
   let x'' := fresh "x''" in
   intro x'';
   let xv := assoc_right_tuple x'' (@None) in
   refine (SmartVarf (xv : interp_flat_type _ t')).
 
-Definition unop_make_args {interp_base_type var} (x : exprArg interp_base_type var) : exprArgRev interp_base_type var.
+Definition unop_make_args {var} (x : exprArg var) : exprArgRev var.
 Proof. make_args x. Defined.
-Definition unop_wire_make_args {interp_base_type var} (x : exprArgWire interp_base_type var) : exprArgWireRev interp_base_type var.
+Definition unop_wire_make_args {var} (x : exprArgWire var) : exprArgWireRev var.
 Proof. make_args x. Defined.
 
 Local Ltac args_to_bounded x H :=
@@ -432,31 +432,31 @@ Defined.
 Definition op9_4_bounds_good (bounds : interp_flat_type (fun _ => ZBounds.bounds) (remove_all_binders Expr9_4OpT)) : bool.
 Proof. make_bounds_prop bounds Expr4Op_bounds. Defined.
 
-Definition ApplyUnOp {interp_base_type var} (f : exprUnOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var
+Definition ApplyUnOp {var} (f : exprUnOp var) : exprArg var -> exprArg var
   := fun x
-     => LetIn (UnReturn (unop_make_args x))
-              (fun k => UnReturn (Apply length_fe25519 f k)).
-Definition ApplyBinOp {interp_base_type var} (f : exprBinOp interp_base_type var) : exprArg interp_base_type var -> exprArg interp_base_type var -> exprArg interp_base_type var
+     => LetIn (invert_Return (unop_make_args x))
+              (fun k => invert_Return (Apply length_fe25519 f k)).
+Definition ApplyBinOp {var} (f : exprBinOp var) : exprArg var -> exprArg var -> exprArg var
   := fun x y
-     => LetIn (UnReturn (unop_make_args x))
+     => LetIn (invert_Return (unop_make_args x))
               (fun x'
-               => LetIn (UnReturn (unop_make_args y))
+               => LetIn (invert_Return (unop_make_args y))
                         (fun y'
-                         => UnReturn (Apply length_fe25519
+                         => invert_Return (Apply length_fe25519
                                             (Apply length_fe25519
                                                    f x') y'))).
-Definition ApplyUnOpFEToWire {interp_base_type var} (f : exprUnOpFEToWire interp_base_type var) : exprArg interp_base_type var -> exprArgWire interp_base_type var
+Definition ApplyUnOpFEToWire {var} (f : exprUnOpFEToWire var) : exprArg var -> exprArgWire var
   := fun x
-     => LetIn (UnReturn (unop_make_args x))
-              (fun k => UnReturn (Apply length_fe25519 f k)).
-Definition ApplyUnOpWireToFE {interp_base_type var} (f : exprUnOpWireToFE interp_base_type var) : exprArgWire interp_base_type var -> exprArg interp_base_type var
+     => LetIn (invert_Return (unop_make_args x))
+              (fun k => invert_Return (Apply length_fe25519 f k)).
+Definition ApplyUnOpWireToFE {var} (f : exprUnOpWireToFE var) : exprArgWire var -> exprArg var
   := fun x
-     => LetIn (UnReturn (unop_wire_make_args x))
-              (fun k => UnReturn (Apply (List.length wire_widths) f k)).
-Definition ApplyUnOpFEToZ {interp_base_type var} (f : exprUnOpFEToZ interp_base_type var) : exprArg interp_base_type var -> exprZ interp_base_type var
+     => LetIn (invert_Return (unop_wire_make_args x))
+              (fun k => invert_Return (Apply (List.length wire_widths) f k)).
+Definition ApplyUnOpFEToZ {var} (f : exprUnOpFEToZ var) : exprArg var -> exprZ var
   := fun x
-     => LetIn (UnReturn (unop_make_args x))
-              (fun k => UnReturn (Apply length_fe25519 f k)).
+     => LetIn (invert_Return (unop_make_args x))
+              (fun k => invert_Return (Apply length_fe25519 f k)).
 
 
 (* FIXME TODO(jgross): This is a horrible tactic.  We should unify the
@@ -545,17 +545,14 @@ Ltac rexpr_correct :=
   assert (wf_ropW : Wf ropW') by (subst ropW' ropZ_sig; reflect_Wf base_type_eq_semidec_is_dec op_beq_bl);
   cbv zeta; repeat apply conj;
   [ vm_compute; reflexivity
-  | apply @InterpRelWf;
-    [ | apply @RelWfMapInterp, wf_ropW ].. ];
+  | apply @InterpWf;
+    [ | apply wf_ropW ].. ];
   auto with interp_related.
 
-Notation rword_of_Z rexprZ_sig := (MapInterp WordW.of_Z (proj1_sig rexprZ_sig)) (only parsing).
-
-Definition rword64ize {t} (x : Expr t) : Expr t
-  := MapInterp (fun t => match t with TZ => word64ize end) x.
+Notation rword_of_Z rexprZ_sig := (proj1_sig rexprZ_sig) (only parsing).
 
 Notation compute_bounds opW bounds
-  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) (MapInterp (@ZBounds.of_wordW) opW)) bounds)
+  := (ApplyInterpedAll (Interp (@ZBounds.interp_op) opW) bounds)
        (only parsing).
 
 
@@ -586,6 +583,7 @@ Module Export PrettyPrinting.
                               | in_range _ _ => no
                               | enlargen _ => borked
                               end
+       | Unit => fun _ => no
        | Prod x y => fun v => match @does_it_overflow _ (fst v), @does_it_overflow _ (snd v) with
                               | no, no => no
                               | yes, no | no, yes | yes, yes => yes
diff --git a/src/Specific/GF25519Reflective/Common9_4Op.v b/src/Specific/GF25519Reflective/Common9_4Op.v
index 5754b8c54..5fbb72c26 100644
--- a/src/Specific/GF25519Reflective/Common9_4Op.v
+++ b/src/Specific/GF25519Reflective/Common9_4Op.v
@@ -3,7 +3,6 @@ Require Import Crypto.Specific.GF25519BoundedCommon.
 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.
diff --git a/src/Specific/GF25519Reflective/CommonBinOp.v b/src/Specific/GF25519Reflective/CommonBinOp.v
index b325a56eb..07c0d82dd 100644
--- a/src/Specific/GF25519Reflective/CommonBinOp.v
+++ b/src/Specific/GF25519Reflective/CommonBinOp.v
@@ -3,7 +3,6 @@ Require Import Crypto.Specific.GF25519BoundedCommon.
 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.
@@ -18,7 +17,7 @@ Lemma ExprBinOp_correct_and_bounded
           let Hy := let (Hx, Hy) := Hxy in Hy in
           let args := binop_args_to_bounded xy Hx Hy 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
@@ -33,12 +32,12 @@ Lemma ExprBinOp_correct_and_bounded
           let args := binop_args_to_bounded (fst xy, snd xy) Hx Hy 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 => binop_bounds_good bounds = true
           | None => False
           end)
-  : binop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+  : binop_correct_and_bounded ropW op.
 Proof.
   intros x y Hx Hy.
   pose x as x'; pose y as y'.
diff --git a/src/Specific/GF25519Reflective/CommonUnOp.v b/src/Specific/GF25519Reflective/CommonUnOp.v
index 10390798b..a55bdc58d 100644
--- a/src/Specific/GF25519Reflective/CommonUnOp.v
+++ b/src/Specific/GF25519Reflective/CommonUnOp.v
@@ -3,7 +3,6 @@ Require Import Crypto.Specific.GF25519BoundedCommon.
 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.
@@ -15,7 +14,7 @@ Lemma ExprUnOp_correct_and_bounded
                    (Hx : is_bounded (fe25519WToZ x) = true),
           let args := unop_args_to_bounded x Hx 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
@@ -27,12 +26,12 @@ Lemma ExprUnOp_correct_and_bounded
           let args := unop_args_to_bounded x Hx 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 => unop_bounds_good bounds = true
           | None => False
           end)
-  : unop_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+  : unop_correct_and_bounded ropW op.
 Proof.
   intros x Hx.
   pose x as x'.
diff --git a/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v b/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v
index 2531e6184..b9395d3ef 100644
--- a/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v
+++ b/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v
@@ -3,7 +3,6 @@ Require Import Crypto.Specific.GF25519BoundedCommon.
 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.
@@ -15,7 +14,7 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
                    (Hx : is_bounded (fe25519WToZ x) = true),
           let args := unop_args_to_bounded x Hx 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
@@ -27,12 +26,12 @@ Lemma ExprUnOpFEToWire_correct_and_bounded
           let args := unop_args_to_bounded x Hx 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 => unopFEToWire_bounds_good bounds = true
           | None => False
           end)
-  : unop_FEToWire_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+  : unop_FEToWire_correct_and_bounded ropW op.
 Proof.
   intros x Hx.
   pose x as x'.
diff --git a/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v b/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v
index 06d53a1e1..55ce98a40 100644
--- a/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v
+++ b/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v
@@ -3,7 +3,6 @@ Require Import Crypto.Specific.GF25519BoundedCommon.
 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.
@@ -15,7 +14,7 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
                    (Hx : is_bounded (fe25519WToZ x) = true),
           let args := unop_args_to_bounded x Hx 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
@@ -27,12 +26,12 @@ Lemma ExprUnOpFEToZ_correct_and_bounded
           let args := unop_args_to_bounded x Hx 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 => unopFEToZ_bounds_good bounds = true
           | None => False
           end)
-  : unop_FEToZ_correct (MapInterp (fun _ x => x) ropW) op.
+  : unop_FEToZ_correct ropW op.
 Proof.
   intros x Hx.
   pose x as x'.
diff --git a/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v b/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v
index d0c46d1ed..023969413 100644
--- a/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v
+++ b/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v
@@ -3,7 +3,6 @@ Require Import Crypto.Specific.GF25519BoundedCommon.
 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.
@@ -15,7 +14,7 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
                    (Hx : wire_digits_is_bounded (wire_digitsWToZ x) = true),
           let args := unopWireToFE_args_to_bounded x Hx 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
@@ -27,12 +26,12 @@ Lemma ExprUnOpWireToFE_correct_and_bounded
           let args := unopWireToFE_args_to_bounded x Hx 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 => unopWireToFE_bounds_good bounds = true
           | None => False
           end)
-  : unop_WireToFE_correct_and_bounded (MapInterp (fun _ x => x) ropW) op.
+  : unop_WireToFE_correct_and_bounded ropW op.
 Proof.
   intros x Hx.
   pose x as x'.
diff --git a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v
index c5becbcca..c80aa7ffa 100644
--- a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v
+++ b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v
@@ -4,6 +4,8 @@ Require Export Crypto.Specific.GF25519.
 Require Export Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.ExprInversion.
+Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.Linearize.
 Require Import Crypto.Reflection.Z.Interpretations64.
@@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify.
 Require Export Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.InterpWfRel.
 Require Import Crypto.Reflection.LinearizeInterp.
-Require Import Crypto.Reflection.MapInterp.
-Require Import Crypto.Reflection.MapInterpWf.
 Require Import Crypto.Reflection.WfReflective.
 Require Import Crypto.CompleteEdwardsCurve.ExtendedCoordinates.
 Require Import Crypto.Specific.GF25519Reflective.Reified.Add.
@@ -36,12 +36,12 @@ Definition radd_coordinatesZ' var twice_d P1 P2
        (fun x y => ApplyBinOp (proj1_sig rsubZ_sig var) x y)
        (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y)
        twice_d _
-       (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr)
-       (fun v f => LetIn (UnReturn v)
+       (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr)
+       (fun v f => LetIn (invert_Return v)
                          (fun k => f (Return (SmartVarf k))))
        P1 P2.
 
-Definition radd_coordinatesZ'' : Syntax.Expr _ _ _ _
+Definition radd_coordinatesZ'' : Syntax.Expr _ _ _
   := Linearize (fun var
                 => apply9
                      (fun A B => SmartAbs (A := A) (B := B))
@@ -79,16 +79,16 @@ Local Ltac repeat_step_interpf :=
   clearbody k'; subst k'.
 
 Lemma interp_helper
-      (f : Syntax.Expr base_type interp_base_type op ExprBinOpT)
-      (x y : exprArg interp_base_type interp_base_type)
+      (f : Syntax.Expr base_type op ExprBinOpT)
+      (x y : exprArg interp_base_type)
       (f' : GF25519.fe25519 -> GF25519.fe25519 -> GF25519.fe25519)
       (x' y' : GF25519.fe25519)
       (H : interp_type_gen_rel_pointwise
              (fun _ => Logic.eq)
              (Interp interp_op f) (uncurry_binop_fe25519 f'))
-      (Hx : interpf interp_op (UnReturn x) = x')
-      (Hy : interpf interp_op (UnReturn y) = y')
-  : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'.
+      (Hx : interpf interp_op (invert_Return x) = x')
+      (Hy : interpf interp_op (invert_Return y) = y')
+  : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'.
 Proof.
   cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe25519 interp_flat_type] in H.
   simpl @interp_base_type in *.
@@ -103,14 +103,14 @@ Proof.
   change (fun t => interp_base_type t) with interp_base_type in *.
   generalize (f interp_base_type); clear f; intro f.
   cbv [Apply length_fe25519 Apply' interp fst snd].
-  rewrite <- (UnAbs_eta f).
+  rewrite (invert_Abs_Some (e:=f) eq_refl).
   repeat match goal with
-         | [ |- appcontext[UnAbs ?f ?x] ]
-           => generalize (UnAbs f x); clear f;
+         | [ |- appcontext[invert_Abs ?f ?x] ]
+           => generalize (invert_Abs f x); clear f;
                 let f' := fresh "f" in
                 intro f';
-                  first [ rewrite <- (UnAbs_eta f')
-                        | rewrite <- (UnReturn_eta f') ]
+                  first [ rewrite (invert_Abs_Some (e:=f') eq_refl)
+                        | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ]
          end.
   reflexivity.
 Qed.
@@ -121,7 +121,7 @@ Proof.
   etransitivity; [ apply Interp_Linearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT radd_coordinatesZ'' uncurried_add_coordinates uncurry_unop_fe25519 SmartAbs radd_coordinatesZ' exprArg Extended.add_coordinates_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519 add_coordinates].
   intros.
-  unfold UnReturn at 13 14 15 16.
+  unfold invert_Return at 13 14 15 16.
   repeat match goal with
          | [ |- appcontext[@proj1_sig ?A ?B ?v] ]
            => let k := fresh "f" in
@@ -144,9 +144,9 @@ Proof.
                 cbv beta; intros
          end;
     repeat match goal with
-           | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ]
+           | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ]
              => apply interp_helper; [ assumption | | ]
-           | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ]
+           | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ]
              => vm_compute; reflexivity
            | [ |- (_, _) = (_, _) ]
              => reflexivity
diff --git a/src/Specific/GF25519Reflective/Reified/LadderStep.v b/src/Specific/GF25519Reflective/Reified/LadderStep.v
index 655188ba0..d888197f2 100644
--- a/src/Specific/GF25519Reflective/Reified/LadderStep.v
+++ b/src/Specific/GF25519Reflective/Reified/LadderStep.v
@@ -4,6 +4,8 @@ Require Export Crypto.Specific.GF25519.
 Require Export Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Relations.
+Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.Linearize.
 Require Import Crypto.Reflection.Z.Interpretations64.
@@ -13,8 +15,6 @@ Require Import Crypto.Reflection.Z.Reify.
 Require Export Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.InterpWfRel.
 Require Import Crypto.Reflection.LinearizeInterp.
-Require Import Crypto.Reflection.MapInterp.
-Require Import Crypto.Reflection.MapInterpWf.
 Require Import Crypto.Reflection.WfReflective.
 Require Import Crypto.Spec.MxDH.
 Require Import Crypto.Specific.GF25519Reflective.Reified.Add.
@@ -38,13 +38,13 @@ Definition rladderstepZ' var (T:=_) (dummy0 dummy1 dummy2 a24 x0 : T) P1 P2
        (fun x y => ApplyBinOp (proj1_sig rmulZ_sig var) x y)
        a24
        _
-       (fun x y z w => (UnReturn x, UnReturn y, UnReturn z, UnReturn w)%expr)
-       (fun v f => LetIn (UnReturn v)
+       (fun x y z w => (invert_Return x, invert_Return y, invert_Return z, invert_Return w)%expr)
+       (fun v f => LetIn (invert_Return v)
                          (fun k => f (Return (SmartVarf k))))
        x0
        P1 P2.
 
-Definition rladderstepZ'' : Syntax.Expr _ _ _ _
+Definition rladderstepZ'' : Syntax.Expr _ _ _
   := Linearize (fun var
                 => apply9
                      (fun A B => SmartAbs (A := A) (B := B))
@@ -83,16 +83,16 @@ Local Ltac repeat_step_interpf :=
   clearbody k'; subst k'.
 
 Lemma interp_helper
-      (f : Syntax.Expr base_type interp_base_type op ExprBinOpT)
-      (x y : exprArg interp_base_type interp_base_type)
+      (f : Syntax.Expr base_type op ExprBinOpT)
+      (x y : exprArg interp_base_type)
       (f' : GF25519.fe25519 -> GF25519.fe25519 -> GF25519.fe25519)
       (x' y' : GF25519.fe25519)
       (H : interp_type_gen_rel_pointwise
              (fun _ => Logic.eq)
              (Interp interp_op f) (uncurry_binop_fe25519 f'))
-      (Hx : interpf interp_op (UnReturn x) = x')
-      (Hy : interpf interp_op (UnReturn y) = y')
-  : interpf interp_op (UnReturn (ApplyBinOp (f interp_base_type) x y)) = f' x' y'.
+      (Hx : interpf interp_op (invert_Return x) = x')
+      (Hy : interpf interp_op (invert_Return y) = y')
+  : interpf interp_op (invert_Return (ApplyBinOp (f interp_base_type) x y)) = f' x' y'.
 Proof.
   cbv [interp_type_gen_rel_pointwise ExprBinOpT uncurry_binop_fe25519 interp_flat_type] in H.
   simpl @interp_base_type in *.
@@ -107,14 +107,15 @@ Proof.
   change (fun t => interp_base_type t) with interp_base_type in *.
   generalize (f interp_base_type); clear f; intro f.
   cbv [Apply length_fe25519 Apply' interp fst snd].
-  rewrite <- (UnAbs_eta f).
+  let f := match goal with f : expr _ _ _ |- _ => f end in
+  rewrite (invert_Abs_Some (e:=f) eq_refl).
   repeat match goal with
-         | [ |- appcontext[UnAbs ?f ?x] ]
-           => generalize (UnAbs f x); clear f;
+         | [ |- appcontext[invert_Abs ?f ?x] ]
+           => generalize (invert_Abs f x); clear f;
                 let f' := fresh "f" in
                 intro f';
-                  first [ rewrite <- (UnAbs_eta f')
-                        | rewrite <- (UnReturn_eta f') ]
+                  first [ rewrite (invert_Abs_Some (e:=f') eq_refl)
+                        | rewrite (invert_Return_Some (e:=f') eq_refl) at 2 ]
          end.
   reflexivity.
 Qed.
@@ -125,7 +126,7 @@ Proof.
   etransitivity; [ apply Interp_Linearize | ].
   cbv beta iota delta [apply9 apply9_nd interp_type_gen_rel_pointwise Expr9_4OpT SmartArrow ExprArgT rladderstepZ'' uncurried_ladderstep uncurry_unop_fe25519 SmartAbs rladderstepZ' exprArg MxDH.ladderstep_gen Interp interp unop_make_args SmartVarf smart_interp_flat_map length_fe25519 ladderstep].
   intros; cbv beta zeta.
-  unfold UnReturn at 14 15 16 17.
+  unfold invert_Return at 14 15 16 17.
   repeat match goal with
          | [ |- appcontext[@proj1_sig ?A ?B ?v] ]
            => let k := fresh "f" in
@@ -148,9 +149,9 @@ Proof.
                 cbv beta; intros
          end;
     repeat match goal with
-           | [ |- interpf interp_op (UnReturn (ApplyBinOp _ _ _)) = _ ]
+           | [ |- interpf interp_op (invert_Return (ApplyBinOp _ _ _)) = _ ]
              => apply interp_helper; [ assumption | | ]
-           | [ |- interpf interp_op (UnReturn (Return (_, _)%expr)) = (_, _) ]
+           | [ |- interpf interp_op (invert_Return (Return (_, _)%expr)) = (_, _) ]
              => vm_compute; reflexivity
            | [ |- (_, _) = (_, _) ]
              => reflexivity
diff --git a/src/Specific/GF25519ReflectiveAddCoordinates.v b/src/Specific/GF25519ReflectiveAddCoordinates.v
index ef7d01eda..955957a11 100644
--- a/src/Specific/GF25519ReflectiveAddCoordinates.v
+++ b/src/Specific/GF25519ReflectiveAddCoordinates.v
@@ -9,7 +9,6 @@ Require Export Crypto.Specific.GF25519.
 Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
-Require Import Crypto.Reflection.MapInterp.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
@@ -43,7 +42,7 @@ Declare Reduction asm_interp_add_coordinates
             WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type WordW.interp_base_type word64ize
             Interp interp interp_flat_type interpf interpf_step interp_flat_type fst snd].
 Ltac asm_interp_add_coordinates
   := cbv beta iota delta
@@ -54,7 +53,7 @@ Ltac asm_interp_add_coordinates
             WordW.interp_op WordW.interp_base_type
             Z.interp_op Z.interp_base_type
             Z.Syntax.interp_op Z.Syntax.interp_base_type
-            mapf_interp_flat_type map_interp WordW.interp_base_type MapInterp mapf_interp word64ize rword64ize
+            mapf_interp_flat_type WordW.interp_base_type word64ize
             Interp interp interp_flat_type interpf interp_flat_type fst snd].
 
 
@@ -68,7 +67,7 @@ Time Definition interp_radd_coordinates : Specific.GF25519BoundedCommon.fe25519W
                                           -> Specific.GF25519BoundedCommon.fe25519W
                                           -> Specific.GF25519BoundedCommon.fe25519W
                                           -> Tuple.tuple Specific.GF25519BoundedCommon.fe25519W 4
-  := Eval asm_interp_add_coordinates in interp_9_4expr (rword64ize radd_coordinates).
+  := Eval asm_interp_add_coordinates in interp_9_4expr radd_coordinates.
 (*Print interp_radd_coordinates.*)
 Time Definition interp_radd_coordinates_correct : interp_radd_coordinates = interp_9_4expr radd_coordinates := eq_refl.