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

1 files changed, 114 insertions, 73 deletions

diff --git a/src/Reflection/ExprInversion.v b/src/Reflection/ExprInversion.v
index 06a4f5b30..c403ed5e6 100644
--- a/src/Reflection/ExprInversion.v
+++ b/src/Reflection/ExprInversion.v
@@ -8,91 +8,132 @@ Require Import Crypto.Util.Notations.
 Section language.
   Context {base_type_code : Type}
           {interp_base_type : base_type_code -> Type}
-          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
-          {var : base_type_code -> Type}.
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}.
 
   Local Notation flat_type := (flat_type base_type_code).
   Local Notation type := (type base_type_code).
-  Local Notation Tbase := (@Tbase base_type_code).
   Local Notation interp_type := (interp_type interp_base_type).
+  Local Notation interp_flat_type_gen := interp_flat_type.
   Local Notation interp_flat_type := (interp_flat_type interp_base_type).
-  Local Notation exprf := (@exprf base_type_code interp_base_type op var).
-  Local Notation expr := (@expr base_type_code interp_base_type op var).
-  Local Notation Expr := (@Expr base_type_code interp_base_type op).
+  Local Notation Expr := (@Expr base_type_code op).
 
-  Definition invert_Const {t} (e : exprf t) : option (interp_type t)
-    := match e with Const _ v => Some v | _ => None end.
-  Definition invert_Var {t} (e : exprf (Tbase t)) : option (var t)
-    := match e in Syntax.exprf _ _ _ t'
-             return option (var match t' with
-                                | Syntax.Tbase t' => t'
-                                | _ => t
-                                end)
-       with
-       | Var _ v => Some v
-       | _ => None
-       end.
-  Definition invert_Op {t} (e : exprf t) : option { t1 : flat_type & op t1 t * exprf t1 }%type
-    := match e with Op _ _ opc args => Some (existT _ _ (opc, args)) | _ => None end.
-  Definition invert_LetIn {A} (e : exprf A) : option { B : _ & exprf B * (Syntax.interp_flat_type var B -> exprf A) }%type
-    := match e in Syntax.exprf _ _ _ t return option { B : _ & _ * (_ -> exprf t) }%type with
-       | LetIn _ ex _ eC => Some (existT _ _ (ex, eC))
-       | _ => None
-       end.
-  Definition invert_Pair {A B} (e : exprf (Prod A B)) : option (exprf A * exprf B)
-    := match e in Syntax.exprf _ _ _ t
-             return option match t with
-                           | Prod _ _ => _
-                           | _ => unit
-                           end with
-       | Pair _ x _ y => Some (x, y)%core
-       | _ => None
+  Fixpoint codomain (t : type) : flat_type
+    := match t with
+       | Tflat T => T
+       | Arrow src dst => codomain dst
        end.
 
-  Local Ltac t' :=
-    repeat first [ intro
-                 | progress simpl in *
-                 | reflexivity
-                 | assumption
-                 | progress destruct_head False
-                 | progress subst
-                 | progress inversion_option
-                 | progress inversion_sigma
-                 | progress break_match ].
-  Local Ltac t :=
-    lazymatch goal with
-    | [ |- _ = Some ?v -> ?e = _ ]
-      => revert v;
-         refine match e with
-                | Const _ _ => _
-                | _ => _
-                end
-    end;
-    t'.
+  Section with_var.
+    Context {var : base_type_code -> Type}.
+
+    Local Notation exprf := (@exprf base_type_code op var).
+    Local Notation expr := (@expr base_type_code op var).
+
+    Definition invert_Var {t} (e : exprf (Tbase t)) : option (var t)
+      := match e in Syntax.exprf _ _ t'
+               return option (var match t' with
+                                  | Tbase t' => t'
+                                  | _ => t
+                                  end)
+         with
+         | Var _ v => Some v
+         | _ => None
+         end.
+    Definition invert_Op {t} (e : exprf t) : option { t1 : flat_type & op t1 t * exprf t1 }%type
+      := match e with Op _ _ opc args => Some (existT _ _ (opc, args)) | _ => None end.
+    Definition invert_LetIn {A} (e : exprf A) : option { B : _ & exprf B * (Syntax.interp_flat_type var B -> exprf A) }%type
+      := match e in Syntax.exprf _ _ t return option { B : _ & _ * (_ -> exprf t) }%type with
+         | LetIn _ ex _ eC => Some (existT _ _ (ex, eC))
+         | _ => None
+         end.
+    Definition invert_Pair {A B} (e : exprf (Prod A B)) : option (exprf A * exprf B)
+      := match e in Syntax.exprf _ _ t
+               return option match t with
+                             | Prod _ _ => _
+                             | _ => unit
+                             end with
+         | Pair _ x _ y => Some (x, y)%core
+         | _ => None
+         end.
+    Definition invert_Abs {A B} (e : expr (Arrow A B)) : var A -> expr B
+      := match e with Abs _ _ f => f end.
+    Definition invert_Return {t} (e : expr (Tflat t)) : exprf t
+      := match e with Return _ v => v end.
+
+    Local Ltac t' :=
+      repeat first [ intro
+                   | progress simpl in *
+                   | reflexivity
+                   | assumption
+                   | progress destruct_head False
+                   | progress subst
+                   | progress inversion_option
+                   | progress inversion_sigma
+                   | progress break_match ].
+    Local Ltac t :=
+      lazymatch goal with
+      | [ |- _ = Some ?v -> ?e = _ ]
+        => revert v;
+           refine match e with
+                  | Var _ _ => _
+                  | _ => _
+                  end
+      | [ |- _ = ?v -> ?e = _ ]
+        => revert v;
+           refine match e with
+                  | Abs _ _ _ => _
+                  | Return _ _ => _
+                  end
+      end;
+      t'.
+
+    Lemma invert_Var_Some {t e v}
+      : @invert_Var t e = Some v -> e = Var v.
+    Proof. t. Defined.
+
+    Lemma invert_Op_Some {t e v}
+      : @invert_Op t e = Some v -> e = Op (fst (projT2 v)) (snd (projT2 v)).
+    Proof. t. Defined.
 
-  Lemma invert_Const_Some {t e v}
-    : @invert_Const t e = Some v -> e = Const v.
-  Proof. t. Defined.
+    Lemma invert_LetIn_Some {t e v}
+      : @invert_LetIn t e = Some v -> e = LetIn (fst (projT2 v)) (snd (projT2 v)).
+    Proof. t. Defined.
 
-  Lemma invert_Var_Some {t e v}
-    : @invert_Var t e = Some v -> e = Var v.
-  Proof. t. Defined.
+    Lemma invert_Pair_Some {A B e v}
+      : @invert_Pair A B e = Some v -> e = Pair (fst v) (snd v).
+    Proof. t. Defined.
 
-  Lemma invert_Op_Some {t e v}
-    : @invert_Op t e = Some v -> e = Op (fst (projT2 v)) (snd (projT2 v)).
-  Proof. t. Defined.
+    Lemma invert_Abs_Some {A B e v}
+      : @invert_Abs A B e = v -> e = Abs v.
+    Proof. t. Defined.
 
-  Lemma invert_LetIn_Some {t e v}
-    : @invert_LetIn t e = Some v -> e = LetIn (fst (projT2 v)) (snd (projT2 v)).
-  Proof. t. Defined.
+    Lemma invert_Return_Some {t e v}
+      : @invert_Return t e = v -> e = Return v.
+    Proof. t. Qed.
+  End with_var.
 
-  Lemma invert_Pair_Some {A B e v}
-    : @invert_Pair A B e = Some v -> e = Pair (fst v) (snd v).
-  Proof. t. Defined.
+  Lemma interpf_invert_Abs interp_op {A B e} x
+    : Syntax.interp interp_op (@invert_Abs interp_base_type A B e x)
+      = Syntax.interp interp_op e x.
+  Proof.
+    refine (match e in expr _ _ t
+                  return match t return expr _ _ t -> _ with
+                         | Arrow src dst
+                           => fun e
+                              => (forall x : interp_base_type src,
+                                     interp _ (invert_Abs e x) = interp _ e x)
+                         | Tflat _ => fun _ => True
+                         end e with
+            | Abs _ _ _ => fun _ => eq_refl
+            | Return _ _ => I
+            end x).
+  Qed.
 End language.
 
-Global Arguments invert_Const {_ _ _ _ _} _.
-Global Arguments invert_Var {_ _ _ _ _} _.
-Global Arguments invert_Op {_ _ _ _ _} _.
-Global Arguments invert_LetIn {_ _ _ _ _} _.
-Global Arguments invert_Pair {_ _ _ _ _ _} _.
+Global Arguments codomain {_} _.
+Global Arguments invert_Var {_ _ _ _} _.
+Global Arguments invert_Op {_ _ _ _} _.
+Global Arguments invert_LetIn {_ _ _ _} _.
+Global Arguments invert_Pair {_ _ _ _ _} _.
+Global Arguments invert_Abs {_ _ _ _ _} _ _.
+Global Arguments invert_Return {_ _ _ _} _.