Split off some bits of Reflection.Syntax

Also split off some bits of Util.Tactics

115 files changed, 555 insertions, 398 deletions

diff --git a/src/Reflection/CommonSubexpressionElimination.v b/src/Reflection/CommonSubexpressionElimination.v
index bb4a2d763..560551f44 100644
--- a/src/Reflection/CommonSubexpressionElimination.v
+++ b/src/Reflection/CommonSubexpressionElimination.v
@@ -1,6 +1,7 @@
 (** * Common Subexpression Elimination for PHOAS Syntax *)
 Require Import Coq.Lists.List.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Util.Tactics Crypto.Util.Bool.
 
 Local Open Scope list_scope.
@@ -126,11 +127,11 @@ Section symbolic.
       : interp_flat_type_gen var t -> interp_flat_type_gen fsvar t
       := smart_interp_flat_map
            (g:=interp_flat_type_gen fsvar)
-           base_type_code (fun t v => (v,
-                                       match replacement with
-                                       | Some sv => sv
-                                       | None => symbolicify_var v xs
-                                       end))
+           (fun t v => (v,
+                        match replacement with
+                        | Some sv => sv
+                        | None => symbolicify_var v xs
+                        end))
            tt
            (fun A B => @pair _ _).
     Fixpoint smart_add_mapping {t : flat_type} (xs : mapping) : interp_flat_type_gen fsvar t -> mapping
diff --git a/src/Reflection/Conversion.v b/src/Reflection/Conversion.v
index f06b7e5b9..77d4eed34 100644
--- a/src/Reflection/Conversion.v
+++ b/src/Reflection/Conversion.v
@@ -1,5 +1,6 @@
 (** * Convert between interpretations of types *)
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Util.Notations Crypto.Util.Tactics.
 
 Local Open Scope expr_scope.
diff --git a/src/Reflection/CountLets.v b/src/Reflection/CountLets.v
index 85b6e3ad7..00aca28ed 100644
--- a/src/Reflection/CountLets.v
+++ b/src/Reflection/CountLets.v
@@ -1,5 +1,6 @@
 (** * Counts how many binders there are *)
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 
 Local Open Scope ctype_scope.
 Section language.
diff --git a/src/Reflection/FilterLive.v b/src/Reflection/FilterLive.v
index 57e296df7..7a22cd9f4 100644
--- a/src/Reflection/FilterLive.v
+++ b/src/Reflection/FilterLive.v
@@ -1,5 +1,6 @@
 (** * Computes a list of live variables *)
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Named.NameUtil.
 Require Import Crypto.Reflection.CountLets.
 Require Import Crypto.Util.ListUtil.
@@ -31,8 +32,8 @@ Section language.
     | nil, ls2 => ls2
     end.
 
-  Definition names_to_list {t} : interp_flat_type (fun _ => Name) t -> list Name
-    := smart_interp_flat_map base_type_code (g:=fun _ => list Name) (fun _ x => x :: nil)%list nil (fun _ _ x y => x ++ y)%list.
+  Definition names_to_list {t} : interp_flat_type (fun _ : base_type_code => Name) t -> list Name
+    := smart_interp_flat_map (g:=fun _ => list Name) (fun _ x => x :: nil)%list nil (fun _ _ x y => x ++ y)%list.
 
   Fixpoint filter_live_namesf (prefix remaining : list Name) {t} (e : exprf t) : list Name
     := match e with
diff --git a/src/Reflection/Inline.v b/src/Reflection/Inline.v
index 91ad0886e..dff686259 100644
--- a/src/Reflection/Inline.v
+++ b/src/Reflection/Inline.v
@@ -1,5 +1,6 @@
 (** * Inline: Remove some [Let] expressions *)
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Util.Tactics.
 
 Local Open Scope ctype_scope.
diff --git a/src/Reflection/InlineInterp.v b/src/Reflection/InlineInterp.v
index 1d92d1480..31dbce4eb 100644
--- a/src/Reflection/InlineInterp.v
+++ b/src/Reflection/InlineInterp.v
@@ -1,5 +1,6 @@
 (** * Inline: Remove some [Let] expressions *)
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.InlineWf.
 Require Import Crypto.Reflection.InterpProofs.
diff --git a/src/Reflection/InlineWf.v b/src/Reflection/InlineWf.v
index 5e402bf97..d721f9ce7 100644
--- a/src/Reflection/InlineWf.v
+++ b/src/Reflection/InlineWf.v
@@ -1,5 +1,6 @@
 (** * Inline: Remove some [Let] expressions *)
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.WfProofs.
 Require Import Crypto.Reflection.Inline.
 Require Import Crypto.Util.Tactics.SpecializeBy Crypto.Util.Tactics.DestructHead Crypto.Util.Sigma Crypto.Util.Prod.
@@ -21,11 +22,11 @@ Section language.
   Section with_var.
     Context {var1 var2 : base_type_code -> Type}.
 
-    Local Hint Constructors Syntax.wff.
+    Local Hint Constructors Wf.wff.
     Local Hint Resolve List.in_app_or List.in_or_app.
 
     Local Hint Constructors or.
-    Local Hint Constructors Syntax.wff.
+    Local Hint Constructors Wf.wff.
     Local Hint Extern 1 => progress unfold List.In in *.
     Local Hint Resolve wff_in_impl_Proper.
     Local Hint Resolve wff_SmartVarf.
diff --git a/src/Reflection/InputSyntax.v b/src/Reflection/InputSyntax.v
index 3cd688cf3..42ac17069 100644
--- a/src/Reflection/InputSyntax.v
+++ b/src/Reflection/InputSyntax.v
@@ -1,6 +1,7 @@
 (** * PHOAS Representation of Gallina which allows exact denotation *)
 Require Import Coq.Strings.String.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.InterpProofs.
 Require Import Crypto.Util.Tuple.
@@ -79,7 +80,7 @@ Section language.
       Fixpoint compilef {t} (e : @exprf (interp_flat_type_gen var) t) : @Syntax.exprf base_type_code op var t
         := match e in exprf t return @Syntax.exprf _ _ _ t with
            | Const _ x => @SmartConst _ x
-           | Var _ x => Syntax.SmartVarf x
+           | Var _ x => SmartMap.SmartVarf x
            | Op _ _ op args => Syntax.Op op (@compilef _ args)
            | LetIn _ ex _ eC => Syntax.LetIn (@compilef _ ex) (fun x => @compilef _ (eC x))
            | Pair _ ex _ ey => Syntax.Pair (@compilef _ ex) (@compilef _ ey)
diff --git a/src/Reflection/InterpProofs.v b/src/Reflection/InterpProofs.v
index abd54ec3b..b0aa20ccf 100644
--- a/src/Reflection/InterpProofs.v
+++ b/src/Reflection/InterpProofs.v
@@ -1,4 +1,6 @@
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.WfProofs.
 Require Import Crypto.Util.LetIn.
 Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod.
@@ -37,7 +39,7 @@ Section language.
         (Hin : List.In
                  (existT (fun t : base_type_code => (exprf base_type_code op (Tbase t) * interp_base_type t)%type)
                          t (x, x'))
-                 (flatten_binding_list (t := t') base_type_code (SmartVarVarf v) v))
+                 (flatten_binding_list (t := t') (SmartVarVarf v) v))
     : interpf interp_op x = x'.
   Proof.
     clear -Hin.
@@ -52,7 +54,7 @@ Section language.
         (Hin : List.In
                  (existT (fun t : base_type_code => (exprf base_type_code op (Tbase t) * interp_base_type t)%type)
                          t (x, x'))
-                 (flatten_binding_list (t := t') base_type_code (SmartVarVarf v') v))
+                 (flatten_binding_list (t := t') (SmartVarVarf v') v))
     : interpf interp_op x = x'.
   Proof.
     subst; eapply interpf_SmartVarVarf; eassumption.
diff --git a/src/Reflection/InterpWf.v b/src/Reflection/InterpWf.v
index c26c1c3ce..50d05d032 100644
--- a/src/Reflection/InterpWf.v
+++ b/src/Reflection/InterpWf.v
@@ -1,5 +1,6 @@
 Require Import Coq.Strings.String Coq.Classes.RelationClasses.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Sigma.
@@ -25,7 +26,7 @@ Section language.
   Lemma eq_in_flatten_binding_list
         {t x x' T e}
         (HIn : List.In (existT (fun t : base_type_code => (interp_base_type t * interp_base_type t)%type) t (x, x')%core)
-                       (flatten_binding_list base_type_code (t:=T) e e))
+                       (flatten_binding_list (t:=T) e e))
     : x = x'.
   Proof.
     induction T; simpl in *; [ | | rewrite List.in_app_iff in HIn ];
diff --git a/src/Reflection/InterpWfRel.v b/src/Reflection/InterpWfRel.v
index eeee8073e..b4cccf9dc 100644
--- a/src/Reflection/InterpWfRel.v
+++ b/src/Reflection/InterpWfRel.v
@@ -1,5 +1,6 @@
 Require Import Coq.Strings.String Coq.Classes.RelationClasses.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Sigma.
@@ -36,7 +37,7 @@ Section language.
         {t x x' T e1 e2}
         (Hpointwise : interp_flat_type_rel_pointwise2 R e1 e2)
         (HIn : List.In (existT (fun t : base_type_code => (interp_base_type1 t * interp_base_type2 t)%type) t (x, x')%core)
-                       (flatten_binding_list base_type_code (t:=T) e1 e2))
+                       (flatten_binding_list (t:=T) e1 e2))
     : R t x x'.
   Proof.
     induction T; simpl in *; try tauto; [ | rewrite List.in_app_iff in HIn ];
diff --git a/src/Reflection/Linearize.v b/src/Reflection/Linearize.v
index 432907d5c..c251c67c7 100644
--- a/src/Reflection/Linearize.v
+++ b/src/Reflection/Linearize.v
@@ -1,5 +1,6 @@
 (** * Linearize: Place all and only operations in let binders *)
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Util.Tactics.
 
 Local Open Scope ctype_scope.
diff --git a/src/Reflection/LinearizeInterp.v b/src/Reflection/LinearizeInterp.v
index ffa7119c6..0f6a161e5 100644
--- a/src/Reflection/LinearizeInterp.v
+++ b/src/Reflection/LinearizeInterp.v
@@ -1,5 +1,6 @@
 (** * Linearize: Place all and only operations in let binders *)
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.LinearizeWf.
 Require Import Crypto.Reflection.InterpProofs.
diff --git a/src/Reflection/LinearizeWf.v b/src/Reflection/LinearizeWf.v
index 3055c7662..03033536e 100644
--- a/src/Reflection/LinearizeWf.v
+++ b/src/Reflection/LinearizeWf.v
@@ -1,5 +1,6 @@
 (** * Linearize: Place all and only operations in let binders *)
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.WfProofs.
 Require Import Crypto.Reflection.Linearize.
 Require Import Crypto.Util.Tactics Crypto.Util.Sigma.
@@ -43,7 +44,7 @@ Section language.
       end.
     Local Ltac t_fin tac := repeat t_fin_step tac.
 
-    Local Hint Constructors Syntax.wff.
+    Local Hint Constructors Wf.wff.
     Local Hint Resolve List.in_app_or List.in_or_app.
 
     Local Ltac small_inversion_helper wf G0 e2 :=
@@ -54,7 +55,7 @@ Section language.
       pattern G0, t0, e1, e2;
       lazymatch goal with
       | [ |- ?retP _ _ _ _ ]
-        => first [ refine (match wf in @Syntax.wff _ _ _ _ G t v1 v2
+        => first [ refine (match wf in @Wf.wff _ _ _ _ G t v1 v2
                                 return match v1 return Prop with
                                        | TT => retP G t v1 v2
                                        | _ => forall P : Prop, P -> P
@@ -62,7 +63,7 @@ Section language.
                           | WfTT _ => _
                           | _ => fun _ p => p
                           end)
-                | refine (match wf in @Syntax.wff _ _ _ _ G t v1 v2
+                | refine (match wf in @Wf.wff _ _ _ _ G t v1 v2
                                 return match v1 return Prop with
                                        | Var _ _ => retP G t v1 v2
                                        | _ => forall P : Prop, P -> P
@@ -70,7 +71,7 @@ Section language.
                           | WfVar _ _ _ _ _ => _
                           | _ => fun _ p => p
                           end)
-                | refine (match wf in @Syntax.wff _ _ _ _ G t v1 v2
+                | refine (match wf in @Wf.wff _ _ _ _ G t v1 v2
                                 return match v1 return Prop with
                                        | Op _ _ _ _ => retP G t v1 v2
                                        | _ => forall P : Prop, P -> P
@@ -78,7 +79,7 @@ Section language.
                           | WfOp _ _ _ _ _ _ _ => _
                           | _ => fun _ p => p
                           end)
-                | refine (match wf in @Syntax.wff _ _ _ _ G t v1 v2
+                | refine (match wf in @Wf.wff _ _ _ _ G t v1 v2
                                 return match v1 return Prop with
                                        | LetIn _ _ _ _ => retP G t v1 v2
                                        | _ => forall P : Prop, P -> P
@@ -86,7 +87,7 @@ Section language.
                           | WfLetIn _ _ _ _ _ _ _ _ _ => _
                           | _ => fun _ p => p
                           end)
-                | refine (match wf in @Syntax.wff _ _ _ _ G t v1 v2
+                | refine (match wf in @Wf.wff _ _ _ _ G t v1 v2
                                 return match v1 return Prop with
                                        | Pair _ _ _ _ => retP G t v1 v2
                                        | _ => forall P : Prop, P -> P
@@ -98,7 +99,7 @@ Section language.
     Fixpoint wff_under_letsf G {t} e1 e2 {tC} eC1 eC2
              (wf : @wff var1 var2 G t e1 e2)
              (H : forall (x1 : interp_flat_type var1 t) (x2 : interp_flat_type var2 t),
-                 wff (flatten_binding_list base_type_code x1 x2 ++ G) (eC1 x1) (eC2 x2))
+                 wff (flatten_binding_list x1 x2 ++ G) (eC1 x1) (eC2 x2))
              {struct e1}
       : @wff var1 var2 G tC (under_letsf e1 eC1) (under_letsf e2 eC2).
     Proof.
diff --git a/src/Reflection/Map.v b/src/Reflection/Map.v
new file mode 100644
index 000000000..9faa69eb9
--- /dev/null
+++ b/src/Reflection/Map.v
@@ -0,0 +1,30 @@
+Require Import Crypto.Reflection.Syntax.
+
+Section language.
+  Context {base_type_code : Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          {var1 var2 : base_type_code -> Type}
+          (fvar12 : forall t, var1 t -> var2 t)
+          (fvar21 : forall t, var2 t -> var1 t).
+  Local Notation exprf := (@exprf base_type_code op).
+  Fixpoint mapf_interp_flat_type {t} (e : interp_flat_type var2 t) {struct t}
+    : interp_flat_type var1 t
+    := match t return interp_flat_type _ t -> interp_flat_type _ t with
+       | Tbase _ => fvar21 _
+       | Unit => fun v : unit => v
+       | Prod x y => fun xy => (@mapf_interp_flat_type _ (fst xy),
+                                @mapf_interp_flat_type _ (snd xy))
+       end e.
+
+  Fixpoint mapf {t} (e : @exprf var1 t) : @exprf var2 t
+    := match e in Syntax.exprf _ _ t return exprf t with
+       | TT => TT
+       | Var _ x => Var (fvar12 _ x)
+       | Op _ _ op args => Op op (@mapf _ args)
+       | LetIn _ ex _ eC => LetIn (@mapf _ ex) (fun x => @mapf _ (eC (mapf_interp_flat_type x)))
+       | Pair _ ex _ ey => Pair (@mapf _ ex) (@mapf _ ey)
+       end.
+End language.
+
+Global Arguments mapf_interp_flat_type {_ _ _} _ {t} _.
+Global Arguments mapf {_ _ _ _} _ _ {t} _.
diff --git a/src/Reflection/MapCast.v b/src/Reflection/MapCast.v
index 758b016f8..8d6d78969 100644
--- a/src/Reflection/MapCast.v
+++ b/src/Reflection/MapCast.v
@@ -1,4 +1,5 @@
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Prod.
diff --git a/src/Reflection/MapCastWithCastOp.v b/src/Reflection/MapCastWithCastOp.v
index ae41e1181..3dcb6f142 100644
--- a/src/Reflection/MapCastWithCastOp.v
+++ b/src/Reflection/MapCastWithCastOp.v
@@ -1,4 +1,5 @@
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Equality.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapCast.
diff --git a/src/Reflection/MultiSizeTest.v b/src/Reflection/MultiSizeTest.v
index eab8a8302..2c7975113 100644
--- a/src/Reflection/MultiSizeTest.v
+++ b/src/Reflection/MultiSizeTest.v
@@ -1,4 +1,5 @@
 Require Import Coq.omega.Omega.
+Require Import Crypto.Reflection.SmartMap.
 
 Set Implicit Arguments.
 Set Asymmetric Patterns.
diff --git a/src/Reflection/MultiSizeTest2.v b/src/Reflection/MultiSizeTest2.v
index da5749f87..8189b1325 100644
--- a/src/Reflection/MultiSizeTest2.v
+++ b/src/Reflection/MultiSizeTest2.v
@@ -1,5 +1,6 @@
 Require Import Coq.omega.Omega.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Equality.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.MapCastWithCastOp.
diff --git a/src/Reflection/Named/EstablishLiveness.v b/src/Reflection/Named/EstablishLiveness.v
index 7822985e1..bd9a46b9a 100644
--- a/src/Reflection/Named/EstablishLiveness.v
+++ b/src/Reflection/Named/EstablishLiveness.v
@@ -1,6 +1,7 @@
 (** * Compute a list of liveness values for each binding *)
 Require Import Coq.Lists.List.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Named.Syntax.
 Require Import Crypto.Reflection.CountLets.
 Require Import Crypto.Util.ListUtil.
diff --git a/src/Reflection/Named/Syntax.v b/src/Reflection/Named/Syntax.v
index f6ce5d1f5..2c1f3bd23 100644
--- a/src/Reflection/Named/Syntax.v
+++ b/src/Reflection/Named/Syntax.v
@@ -1,6 +1,7 @@
 (** * Named Representation of Gallina *)
 Require Import Coq.Classes.RelationClasses.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Util.PointedProp.
 Require Import Crypto.Util.Tuple.
 Require Import Crypto.Util.Tactics.
@@ -54,7 +55,7 @@ Module Export Named.
           pair-projections and [Pair] as necessary to handle
           [flat_type], and not just [base_type_code] *)
         Definition SmartVar {t} : interp_flat_type_gen (fun _ => Name) t -> exprf t
-          := smart_interp_flat_map (f:=fun _ => Name) (g:=exprf) _ (fun t => Var) TT (fun A B x y => Pair x y).
+          := smart_interp_flat_map (f:=fun _ => Name) (g:=exprf) (fun t => Var) TT (fun A B x y => Pair x y).
       End expr.
 
       Section with_context.
@@ -88,7 +89,6 @@ Module Export Named.
         Definition lookup (ctx : Context) {t}
           : interp_flat_type_gen (fun _ => Name) t -> option (interp_flat_type_gen var t)
           := smart_interp_flat_map
-               base_type_code
                (g := fun t => option (interp_flat_type_gen var t))
                (fun t v => lookupb ctx v)
                (Some tt)
diff --git a/src/Reflection/Relations.v b/src/Reflection/Relations.v
index cd5d174a3..41281b7cc 100644
--- a/src/Reflection/Relations.v
+++ b/src/Reflection/Relations.v
@@ -1,5 +1,6 @@
-Require Import Coq.Classes.RelationClasses Coq.Classes.Morphisms.
+Require Import Coq.Lists.List Coq.Classes.RelationClasses Coq.Classes.Morphisms.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Sigma.
@@ -187,7 +188,7 @@ Section language.
 
   Lemma interp_flat_type_rel_pointwise2_hetero_flatten_binding_list2
         {interp_base_type1 interp_base_type2 t1 t2 T1 T2} R' e1 e2 v1 v2
-        (H : List.In (existT _ (t1, t2)%core (v1, v2)%core) (flatten_binding_list2 base_type_code e1 e2))
+        (H : List.In (existT _ (t1, t2)%core (v1, v2)%core) (flatten_binding_list2 e1 e2))
         (HR : interp_flat_type_rel_pointwise2_hetero interp_base_type1 interp_base_type2 R' T1 T2 e1 e2)
     : R' t1 t2 v1 v2.
   Proof.
diff --git a/src/Reflection/SmartMap.v b/src/Reflection/SmartMap.v
new file mode 100644
index 000000000..cc6c45167
--- /dev/null
+++ b/src/Reflection/SmartMap.v
@@ -0,0 +1,236 @@
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Util.Tactics.RewriteHyp.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Notations.
+
+Section homogenous_type.
+  Context {base_type_code : Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}
+          {var : base_type_code -> Type}.
+
+  Local Notation flat_type := (flat_type base_type_code).
+  Local Notation type := (type base_type_code).
+  Local Notation interp_flat_type := (@interp_flat_type base_type_code).
+  Local Notation exprf := (@exprf base_type_code op var).
+  Local Notation expr := (@expr base_type_code op var).
+  Let Tbase := (@Tbase base_type_code).
+  Local Coercion Tbase : base_type_code >-> flat_type.
+
+  (** Sometimes, we want to deal with partially-interpreted
+      expressions, things like [prod (exprf A) (exprf B)] rather than
+      [exprf (Prod A B)], or like [prod (var A) (var B)] when we start
+      with the type [Prod A B].  These convenience functions let us
+      recurse on the type in only one place, and replace one kind of
+      pairing operator (be it [pair] or [Pair] or anything else) with
+      another kind, and simultaneously mapping a function over the
+      base values (e.g., [Var] (for turning [var] into [exprf]) or
+      [Const] (for turning [interp_base_type] into [exprf])). *)
+
+  Fixpoint smart_interp_flat_map {f g}
+           (h : forall x, f x -> g (Tbase x))
+           (tt : g Unit)
+           (pair : forall A B, g A -> g B -> g (Prod A B))
+           {t}
+    : interp_flat_type f t -> g t
+    := match t return interp_flat_type f t -> g t with
+       | Syntax.Tbase _ => h _
+       | Unit => fun _ => tt
+       | Prod A B => fun v => pair _ _
+                                   (@smart_interp_flat_map f g h tt pair A (fst v))
+                                   (@smart_interp_flat_map f g h tt pair B (snd v))
+       end.
+  Fixpoint smart_interp_flat_map2 {f1 f2 g}
+           (h : forall x, f1 x -> f2 x -> g (Tbase x))
+           (tt : g Unit)
+           (pair : forall A B, g A -> g B -> g (Prod A B))
+           {t}
+    : interp_flat_type f1 t -> interp_flat_type f2 t -> g t
+    := match t return interp_flat_type f1 t -> interp_flat_type f2 t -> g t with
+       | Syntax.Tbase _ => h _
+       | Unit => fun _ _ => tt
+       | Prod A B => fun v1 v2 => pair _ _
+                                       (@smart_interp_flat_map2 f1 f2 g h tt pair A (fst v1) (fst v2))
+                                       (@smart_interp_flat_map2 f1 f2 g h tt pair B (snd v1) (snd v2))
+       end.
+  Fixpoint smart_interp_map_hetero {f g g'}
+           (h : forall x, f x -> g (Tflat (Tbase x)))
+           (tt : g Unit)
+           (pair : forall A B, g (Tflat A) -> g (Tflat B) -> g (Prod A B))
+           (abs : forall A B, (g' A -> g B) -> g (Arrow A B))
+           {t}
+    : interp_type_gen_hetero g' (interp_flat_type f) t -> g t
+    := match t return interp_type_gen_hetero g' (interp_flat_type f) t -> g t with
+       | Tflat _ => @smart_interp_flat_map f (fun x => g (Tflat x)) h tt pair _
+       | Arrow A B => fun v => abs _ _
+                                   (fun x => @smart_interp_map_hetero f g g' h tt pair abs B (v x))
+       end.
+  Fixpoint smart_interp_map_gen {f g}
+           (h : forall x, f x -> g (Tflat (Tbase x)))
+           (h' : forall x, g (Tflat (Tbase x)) -> f x)
+           (flat_map : forall t, interp_flat_type f t -> g t)
+           (abs : forall A B, (g (Tflat (Tbase A)) -> g B) -> g (Arrow A B))
+           {t}
+    : interp_type_gen (interp_flat_type f) t -> g t
+    := match t return interp_type_gen (interp_flat_type f) t -> g t with
+       | Tflat T => flat_map T
+       | Arrow A B => fun v => abs _ _
+                                   (fun x => @smart_interp_map_gen f g h h' flat_map abs B (v (h' _ x)))
+       end.
+  Definition smart_interp_map {f g}
+             (h : forall x, f x -> g (Tflat (Tbase x)))
+             (h' : forall x, g (Tflat (Tbase x)) -> f x)
+             (tt : g Unit)
+             (pair : forall A B, g (Tflat A) -> g (Tflat B) -> g (Prod A B))
+             (abs : forall A B, (g (Tflat (Tbase A)) -> g B) -> g (Arrow A B))
+             {t}
+    : interp_type_gen (interp_flat_type f) t -> g t
+    := @smart_interp_map_gen f g h h' (@smart_interp_flat_map f (fun x => g (Tflat x)) h tt pair) abs t.
+  Fixpoint SmartValf {T} (val : forall t : base_type_code, T t) t : interp_flat_type T t
+    := match t return interp_flat_type T t with
+       | Syntax.Tbase _ => val _
+       | Unit => tt
+       | Prod A B => (@SmartValf T val A, @SmartValf T val B)
+       end.
+  Fixpoint SmartArrow (A : flat_type) (B : type) : type
+    := match A with
+       | Syntax.Tbase A' => Arrow A' B
+       | Unit => B
+       | Prod A0 A1
+         => SmartArrow A0 (SmartArrow A1 B)
+       end.
+  Fixpoint SmartAbs {A B} {struct A} : forall (f : exprf A -> expr B), expr (SmartArrow A B)
+    := match A return (exprf A -> expr B) -> expr (SmartArrow A B) with
+       | Syntax.Tbase x => fun f => Abs (fun x => f (Var x))
+       | Unit => fun f => f TT
+       | Prod x y => fun f => @SmartAbs x _ (fun x' => @SmartAbs y _ (fun y' => f (Pair x' y')))
+       end.
+
+  (** [SmartVar] is like [Var], except that it inserts
+          pair-projections and [Pair] as necessary to handle
+          [flat_type], and not just [base_type_code] *)
+  Definition SmartPairf {t} : interp_flat_type exprf t -> exprf t
+    := @smart_interp_flat_map exprf exprf (fun t x => x) TT (fun A B x y => Pair x y) t.
+  Definition SmartVarf {t} : interp_flat_type var t -> exprf t
+    := @smart_interp_flat_map var exprf (fun t => Var) TT (fun A B x y => Pair x y) t.
+  Definition SmartVarfMap {var var'} (f : forall t, var t -> var' t) {t}
+    : interp_flat_type var t -> interp_flat_type var' t
+    := @smart_interp_flat_map var (interp_flat_type var') f tt (fun A B x y => pair x y) t.
+  Lemma SmartVarfMap_id {var' t} x : @SmartVarfMap var' var' (fun _ x => x) t x = x.
+  Proof.
+    unfold SmartVarfMap; induction t; simpl; destruct_head_hnf unit; destruct_head_hnf prod;
+      rewrite_hyp ?*; congruence.
+  Qed.
+  Definition SmartVarfMap2 {var var' var''} (f : forall t, var t -> var' t -> var'' t) {t}
+    : interp_flat_type var t -> interp_flat_type var' t -> interp_flat_type var'' t
+    := @smart_interp_flat_map2 var var' (interp_flat_type var'') f tt (fun A B x y => pair x y) t.
+  Definition SmartVarfTypeMap {var} (f : forall t, var t -> Type) {t}
+    : interp_flat_type var t -> Type
+    := @smart_interp_flat_map var (fun _ => Type) f unit (fun _ _ P Q => P * Q)%type t.
+  Definition SmartVarfPropMap {var} (f : forall t, var t -> Prop) {t}
+    : interp_flat_type var t -> Prop
+    := @smart_interp_flat_map var (fun _ => Prop) f True (fun _ _ P Q => P /\ Q)%type t.
+  Definition SmartVarfTypeMap2 {var var'} (f : forall t, var t -> var' t -> Type) {t}
+    : interp_flat_type var t -> interp_flat_type var' t -> Type
+    := @smart_interp_flat_map2 var var' (fun _ => Type) f unit (fun _ _ P Q => P * Q)%type t.
+  Definition SmartVarfPropMap2 {var var'} (f : forall t, var t -> var' t -> Prop) {t}
+    : interp_flat_type var t -> interp_flat_type var' t -> Prop
+    := @smart_interp_flat_map2 var var' (fun _ => Prop) f True (fun _ _ P Q => P /\ Q)%type t.
+  Definition SmartFlatTypeMap {var'} (f : forall t, var' t -> base_type_code) {t}
+    : interp_flat_type var' t -> flat_type
+    := @smart_interp_flat_map var' (fun _ => flat_type) f Unit (fun _ _ => Prod) t.
+  Definition SmartFlatTypeUnMap (t : flat_type)
+    : interp_flat_type (fun _ => base_type_code) t
+    := SmartValf (fun t => t) t.
+  Fixpoint SmartFlatTypeMapInterp {var' var''} (f : forall t, var' t -> base_type_code)
+           (fv : forall t v, var'' (f t v)) t {struct t}
+    : forall v, interp_flat_type var'' (SmartFlatTypeMap f (t:=t) v)
+    := match t return forall v, interp_flat_type var'' (SmartFlatTypeMap f (t:=t) v) with
+       | Syntax.Tbase x => fv _
+       | Unit => fun v => v
+       | Prod A B => fun xy => (@SmartFlatTypeMapInterp _ _ f fv A (fst xy),
+                                @SmartFlatTypeMapInterp _ _ f fv B (snd xy))
+       end.
+  Fixpoint SmartFlatTypeMapUnInterp var' var'' var''' (f : forall t, var' t -> base_type_code)
+           (fv : forall t (v : var' t), var'' (f t v) -> var''' t)
+           {t} {struct t}
+    : forall v, interp_flat_type var'' (SmartFlatTypeMap f (t:=t) v)
+                -> interp_flat_type var''' t
+    := match t return forall v, interp_flat_type var'' (SmartFlatTypeMap f (t:=t) v)
+                                -> interp_flat_type var''' t with
+       | Syntax.Tbase x => fv _
+       | Unit => fun _ v => v
+       | Prod A B => fun v xy => (@SmartFlatTypeMapUnInterp _ _ _ f fv A _ (fst xy),
+                                  @SmartFlatTypeMapUnInterp _ _ _ f fv B _ (snd xy))
+       end.
+  Definition SmartVarMap {var var'} (f : forall t, var t -> var' t) (f' : forall t, var' t -> var t) {t}
+    : interp_type_gen (interp_flat_type var) t -> interp_type_gen (interp_flat_type var') t
+    := @smart_interp_map var (interp_type_gen (interp_flat_type var')) f f' tt (fun A B x y => pair x y) (fun A B f x => f x) t.
+  Definition SmartVarMap_hetero {vars vars' var var'} (f : forall t, var t -> var' t) (f' : forall t, vars' t -> vars t) {t}
+    : interp_type_gen_hetero vars (interp_flat_type var) t -> interp_type_gen_hetero vars' (interp_flat_type var') t
+    := @smart_interp_map_hetero var (interp_type_gen_hetero vars' (interp_flat_type var')) vars f tt (fun A B x y => pair x y) (fun A B f x => f (f' _ x)) t.
+  Definition SmartVarVarf {t} : interp_flat_type var t -> interp_flat_type exprf t
+    := SmartVarfMap (fun t => Var).
+(*Definition SmartConstf {t} : interp_flat_type t -> interp_flat_type exprf t
+        := SmartVarfMap (fun t => Const (t:=t)).*)
+End homogenous_type.
+
+Global Arguments SmartVarf {_ _ _ _} _.
+Global Arguments SmartPairf {_ _ _ t} _.
+Global Arguments SmartValf {_} T _ t.
+Global Arguments SmartVarVarf {_ _ _ _} _.
+Global Arguments SmartVarfMap {_ _ _} _ {_} _.
+Global Arguments SmartVarfMap2 {_ _ _ _} _ {t} _ _.
+Global Arguments SmartVarfTypeMap {_ _} _ {_} _.
+Global Arguments SmartVarfPropMap {_ _} _ {_} _.
+Global Arguments SmartVarfTypeMap2 {_ _ _} _ {t} _ _.
+Global Arguments SmartVarfPropMap2 {_ _ _} _ {t} _ _.
+Global Arguments SmartFlatTypeMap {_ _} _ {_} _.
+Global Arguments SmartFlatTypeUnMap {_} _.
+Global Arguments SmartFlatTypeMapInterp {_ _ _ _} _ {_} _.
+Global Arguments SmartFlatTypeMapUnInterp {_ _ _ _ _} fv {_ _} _.
+Global Arguments SmartVarMap_hetero {_ _ _ _ _} _ _ {_} _.
+Global Arguments SmartVarMap {_ _ _} _ _ {_} _.
+(*Global Arguments SmartConstf {_ _ _ _ _} _.*)
+Global Arguments SmartAbs {_ _ _ _ _} _.
+
+Section hetero_type.
+  Fixpoint flatten_flat_type {base_type_code} (t : flat_type (flat_type base_type_code)) : flat_type base_type_code
+    := match t with
+       | Tbase T => T
+       | Unit => Unit
+       | Prod A B => Prod (@flatten_flat_type _ A) (@flatten_flat_type _ B)
+       end.
+
+  Section smart_flat_type_map2.
+    Context {base_type_code1 base_type_code2 : Type}.
+
+    Definition SmartFlatTypeMap2 {var' : base_type_code1 -> Type} (f : forall t, var' t -> flat_type base_type_code2) {t}
+      : interp_flat_type var' t -> flat_type base_type_code2
+      := @smart_interp_flat_map base_type_code1 var' (fun _ => flat_type base_type_code2) f Unit (fun _ _ => Prod) t.
+    Fixpoint SmartFlatTypeMapInterp2 {var' var''} (f : forall t, var' t -> flat_type base_type_code2)
+             (fv : forall t v, interp_flat_type var'' (f t v)) t {struct t}
+      : forall v, interp_flat_type var'' (SmartFlatTypeMap2 f (t:=t) v)
+      := match t return forall v, interp_flat_type var'' (SmartFlatTypeMap2 f (t:=t) v) with
+         | Tbase x => fv _
+         | Unit => fun v => v
+         | Prod A B => fun xy => (@SmartFlatTypeMapInterp2 _ _ f fv A (fst xy),
+                                  @SmartFlatTypeMapInterp2 _ _ f fv B (snd xy))
+         end.
+    Fixpoint SmartFlatTypeMapUnInterp2 var' var'' var''' (f : forall t, var' t -> flat_type base_type_code2)
+             (fv : forall t (v : var' t), interp_flat_type var'' (f t v) -> var''' t)
+             {t} {struct t}
+      : forall v, interp_flat_type var'' (SmartFlatTypeMap2 f (t:=t) v)
+                  -> interp_flat_type var''' t
+      := match t return forall v, interp_flat_type var'' (SmartFlatTypeMap2 f (t:=t) v)
+                                  -> interp_flat_type var''' t with
+         | Tbase x => fv _
+         | Unit => fun _ v => v
+         | Prod A B => fun v xy => (@SmartFlatTypeMapUnInterp2 _ _ _ f fv A _ (fst xy),
+                                    @SmartFlatTypeMapUnInterp2 _ _ _ f fv B _ (snd xy))
+         end.
+  End smart_flat_type_map2.
+End hetero_type.
+
+Global Arguments SmartFlatTypeMap2 {_ _ _} _ {_} _.
+Global Arguments SmartFlatTypeMapInterp2 {_ _ _ _ _} _ {_} _.
+Global Arguments SmartFlatTypeMapUnInterp2 {_ _ _ _ _ _} fv {_ _} _.
diff --git a/src/Reflection/Syntax.v b/src/Reflection/Syntax.v
index 1545114f3..ee60265e0 100644
--- a/src/Reflection/Syntax.v
+++ b/src/Reflection/Syntax.v
@@ -1,7 +1,5 @@
 (** * PHOAS Representation of Gallina *)
-Require Import Coq.Strings.String Coq.Classes.RelationClasses Coq.Classes.Morphisms.
 Require Import Crypto.Util.LetIn.
-Require Import Crypto.Util.Tactics.
 Require Import Crypto.Util.Notations.
 
 (** We parameterize the language over a type of basic type codes (for
@@ -88,162 +86,6 @@ Section language.
       | Abs {src dst} (f : var src -> expr dst) : expr (Arrow src dst).
       Bind Scope expr_scope with expr.
       Global Coercion Return : exprf >-> expr.
-      (** Sometimes, we want to deal with partially-interpreted
-          expressions, things like [prod (exprf A) (exprf B)] rather
-          than [exprf (Prod A B)], or like [prod (var A) (var B)] when
-          we start with the type [Prod A B].  These convenience
-          functions let us recurse on the type in only one place, and
-          replace one kind of pairing operator (be it [pair] or [Pair]
-          or anything else) with another kind, and simultaneously
-          mapping a function over the base values (e.g., [Var] (for
-          turning [var] into [exprf]) or [Const] (for turning
-          [interp_base_type] into [exprf])). *)
-      Fixpoint smart_interp_flat_map {f g}
-               (h : forall x, f x -> g (Tbase x))
-               (tt : g Unit)
-               (pair : forall A B, g A -> g B -> g (Prod A B))
-               {t}
-        : interp_flat_type_gen f t -> g t
-        := match t return interp_flat_type_gen f t -> g t with
-           | Tbase _ => h _
-           | Unit => fun _ => tt
-           | Prod A B => fun v => pair _ _
-                                       (@smart_interp_flat_map f g h tt pair A (fst v))
-                                       (@smart_interp_flat_map f g h tt pair B (snd v))
-           end.
-      Fixpoint smart_interp_flat_map2 {f1 f2 g}
-               (h : forall x, f1 x -> f2 x -> g (Tbase x))
-               (tt : g Unit)
-               (pair : forall A B, g A -> g B -> g (Prod A B))
-               {t}
-        : interp_flat_type_gen f1 t -> interp_flat_type_gen f2 t -> g t
-        := match t return interp_flat_type_gen f1 t -> interp_flat_type_gen f2 t -> g t with
-           | Tbase _ => h _
-           | Unit => fun _ _ => tt
-           | Prod A B => fun v1 v2 => pair _ _
-                                           (@smart_interp_flat_map2 f1 f2 g h tt pair A (fst v1) (fst v2))
-                                           (@smart_interp_flat_map2 f1 f2 g h tt pair B (snd v1) (snd v2))
-           end.
-      Fixpoint smart_interp_map_hetero {f g g'}
-               (h : forall x, f x -> g (Tflat (Tbase x)))
-               (tt : g Unit)
-               (pair : forall A B, g (Tflat A) -> g (Tflat B) -> g (Prod A B))
-               (abs : forall A B, (g' A -> g B) -> g (Arrow A B))
-               {t}
-        : interp_type_gen_hetero g' (interp_flat_type_gen f) t -> g t
-        := match t return interp_type_gen_hetero g' (interp_flat_type_gen f) t -> g t with
-           | Tflat _ => @smart_interp_flat_map f (fun x => g (Tflat x)) h tt pair _
-           | Arrow A B => fun v => abs _ _
-                                       (fun x => @smart_interp_map_hetero f g g' h tt pair abs B (v x))
-           end.
-      Fixpoint smart_interp_map_gen {f g}
-                 (h : forall x, f x -> g (Tflat (Tbase x)))
-                 (h' : forall x, g (Tflat (Tbase x)) -> f x)
-                 (flat_map : forall t, interp_flat_type_gen f t -> g t)
-                 (abs : forall A B, (g (Tflat (Tbase A)) -> g B) -> g (Arrow A B))
-                 {t}
-        : interp_type_gen (interp_flat_type_gen f) t -> g t
-        := match t return interp_type_gen (interp_flat_type_gen f) t -> g t with
-           | Tflat T => flat_map T
-           | Arrow A B => fun v => abs _ _
-                                       (fun x => @smart_interp_map_gen f g h h' flat_map abs B (v (h' _ x)))
-           end.
-      Definition smart_interp_map {f g}
-                 (h : forall x, f x -> g (Tflat (Tbase x)))
-                 (h' : forall x, g (Tflat (Tbase x)) -> f x)
-                 (tt : g Unit)
-                 (pair : forall A B, g (Tflat A) -> g (Tflat B) -> g (Prod A B))
-                 (abs : forall A B, (g (Tflat (Tbase A)) -> g B) -> g (Arrow A B))
-                 {t}
-        : interp_type_gen (interp_flat_type_gen f) t -> g t
-        := @smart_interp_map_gen f g h h' (@smart_interp_flat_map f (fun x => g (Tflat x)) h tt pair) abs t.
-      Fixpoint SmartValf {T} (val : forall t : base_type_code, T t) t : interp_flat_type_gen T t
-        := match t return interp_flat_type_gen T t with
-           | Tbase _ => val _
-           | Unit => tt
-           | Prod A B => (@SmartValf T val A, @SmartValf T val B)
-           end.
-      Fixpoint SmartArrow (A : flat_type) (B : type) : type
-        := match A with
-           | Tbase A' => Arrow A' B
-           | Unit => B
-           | Prod A0 A1
-             => SmartArrow A0 (SmartArrow A1 B)
-           end.
-      Fixpoint SmartAbs {A B} {struct A} : forall (f : exprf A -> expr B), expr (SmartArrow A B)
-        := match A return (exprf A -> expr B) -> expr (SmartArrow A B) with
-           | Tbase x => fun f => Abs (fun x => f (Var x))
-           | Unit => fun f => f TT
-           | Prod x y => fun f => @SmartAbs x _ (fun x' => @SmartAbs y _ (fun y' => f (Pair x' y')))
-           end.
-
-      (** [SmartVar] is like [Var], except that it inserts
-          pair-projections and [Pair] as necessary to handle
-          [flat_type], and not just [base_type_code] *)
-      Definition SmartPairf {t} : interp_flat_type_gen exprf t -> exprf t
-        := @smart_interp_flat_map exprf exprf (fun t x => x) TT (fun A B x y => Pair x y) t.
-      Definition SmartVarf {t} : interp_flat_type_gen var t -> exprf t
-        := @smart_interp_flat_map var exprf (fun t => Var) TT (fun A B x y => Pair x y) t.
-      Definition SmartVarfMap {var var'} (f : forall t, var t -> var' t) {t}
-        : interp_flat_type_gen var t -> interp_flat_type_gen var' t
-        := @smart_interp_flat_map var (interp_flat_type_gen var') f tt (fun A B x y => pair x y) t.
-      Lemma SmartVarfMap_id {var' t} x : @SmartVarfMap var' var' (fun _ x => x) t x = x.
-      Proof.
-        unfold SmartVarfMap; induction t; simpl; destruct_head_hnf unit; destruct_head_hnf prod;
-          rewrite_hyp ?*; congruence.
-      Qed.
-      Definition SmartVarfMap2 {var var' var''} (f : forall t, var t -> var' t -> var'' t) {t}
-        : interp_flat_type_gen var t -> interp_flat_type_gen var' t -> interp_flat_type_gen var'' t
-        := @smart_interp_flat_map2 var var' (interp_flat_type_gen var'') f tt (fun A B x y => pair x y) t.
-      Definition SmartVarfTypeMap {var} (f : forall t, var t -> Type) {t}
-        : interp_flat_type_gen var t -> Type
-        := @smart_interp_flat_map var (fun _ => Type) f unit (fun _ _ P Q => P * Q)%type t.
-      Definition SmartVarfPropMap {var} (f : forall t, var t -> Prop) {t}
-        : interp_flat_type_gen var t -> Prop
-        := @smart_interp_flat_map var (fun _ => Prop) f True (fun _ _ P Q => P /\ Q)%type t.
-      Definition SmartVarfTypeMap2 {var var'} (f : forall t, var t -> var' t -> Type) {t}
-        : interp_flat_type_gen var t -> interp_flat_type_gen var' t -> Type
-        := @smart_interp_flat_map2 var var' (fun _ => Type) f unit (fun _ _ P Q => P * Q)%type t.
-      Definition SmartVarfPropMap2 {var var'} (f : forall t, var t -> var' t -> Prop) {t}
-        : interp_flat_type_gen var t -> interp_flat_type_gen var' t -> Prop
-        := @smart_interp_flat_map2 var var' (fun _ => Prop) f True (fun _ _ P Q => P /\ Q)%type t.
-      Definition SmartFlatTypeMap {var'} (f : forall t, var' t -> base_type_code) {t}
-        : interp_flat_type_gen var' t -> flat_type
-        := @smart_interp_flat_map var' (fun _ => flat_type) f Unit (fun _ _ => Prod) t.
-      Definition SmartFlatTypeUnMap (t : flat_type)
-        : interp_flat_type_gen (fun _ => base_type_code) t
-        := SmartValf (fun t => t) t.
-      Fixpoint SmartFlatTypeMapInterp {var' var''} (f : forall t, var' t -> base_type_code)
-                 (fv : forall t v, var'' (f t v)) t {struct t}
-        : forall v, interp_flat_type_gen var'' (SmartFlatTypeMap f (t:=t) v)
-        := match t return forall v, interp_flat_type_gen var'' (SmartFlatTypeMap f (t:=t) v) with
-           | Tbase x => fv _
-           | Unit => fun v => v
-           | Prod A B => fun xy => (@SmartFlatTypeMapInterp _ _ f fv A (fst xy),
-                                    @SmartFlatTypeMapInterp _ _ f fv B (snd xy))
-           end.
-      Fixpoint SmartFlatTypeMapUnInterp var' var'' var''' (f : forall t, var' t -> base_type_code)
-               (fv : forall t (v : var' t), var'' (f t v) -> var''' t)
-               {t} {struct t}
-        : forall v, interp_flat_type_gen var'' (SmartFlatTypeMap f (t:=t) v)
-                    -> interp_flat_type_gen var''' t
-        := match t return forall v, interp_flat_type_gen var'' (SmartFlatTypeMap f (t:=t) v)
-                                    -> interp_flat_type_gen var''' t with
-           | Tbase x => fv _
-           | Unit => fun _ v => v
-           | Prod A B => fun v xy => (@SmartFlatTypeMapUnInterp _ _ _ f fv A _ (fst xy),
-                                      @SmartFlatTypeMapUnInterp _ _ _ f fv B _ (snd xy))
-           end.
-      Definition SmartVarMap {var var'} (f : forall t, var t -> var' t) (f' : forall t, var' t -> var t) {t}
-        : interp_type_gen (interp_flat_type_gen var) t -> interp_type_gen (interp_flat_type_gen var') t
-        := @smart_interp_map var (interp_type_gen (interp_flat_type_gen var')) f f' tt (fun A B x y => pair x y) (fun A B f x => f x) t.
-      Definition SmartVarMap_hetero {vars vars' var var'} (f : forall t, var t -> var' t) (f' : forall t, vars' t -> vars t) {t}
-        : interp_type_gen_hetero vars (interp_flat_type_gen var) t -> interp_type_gen_hetero vars' (interp_flat_type_gen var') t
-        := @smart_interp_map_hetero var (interp_type_gen_hetero vars' (interp_flat_type_gen var')) vars f tt (fun A B x y => pair x y) (fun A B f x => f (f' _ x)) t.
-      Definition SmartVarVarf {t} : interp_flat_type_gen var t -> interp_flat_type_gen exprf t
-        := SmartVarfMap (fun t => Var).
-      (*Definition SmartConstf {t} : interp_flat_type t -> interp_flat_type_gen exprf t
-        := SmartVarfMap (fun t => Const (t:=t)).*)
     End expr.
 
     Definition Expr (t : type) := forall var, @expr var t.
@@ -273,80 +115,6 @@ Section language.
 
       Definition Interp {t} (E : Expr t) : interp_type t := interp (E _).
     End interp.
-
-    Section map.
-      Context {var1 var2 : base_type_code -> Type}.
-      Context (fvar12 : forall t, var1 t -> var2 t)
-              (fvar21 : forall t, var2 t -> var1 t).
-
-      Fixpoint mapf_interp_flat_type {t} (e : interp_flat_type_gen var2 t) {struct t}
-        : interp_flat_type_gen var1 t
-        := match t return interp_flat_type_gen _ t -> interp_flat_type_gen _ t with
-           | Tbase _ => fvar21 _
-           | Unit => fun v : unit => v
-           | Prod x y => fun xy => (@mapf_interp_flat_type _ (fst xy),
-                                    @mapf_interp_flat_type _ (snd xy))
-           end e.
-
-      Fixpoint mapf {t} (e : @exprf var1 t) : @exprf var2 t
-        := match e in exprf t return exprf t with
-           | TT => TT
-           | Var _ x => Var (fvar12 _ x)
-           | Op _ _ op args => Op op (@mapf _ args)
-           | LetIn _ ex _ eC => LetIn (@mapf _ ex) (fun x => @mapf _ (eC (mapf_interp_flat_type x)))
-           | Pair _ ex _ ey => Pair (@mapf _ ex) (@mapf _ ey)
-           end.
-    End map.
-
-    Section wf.
-      Context {var1 var2 : base_type_code -> Type}.
-
-      Local Notation eP2 := (fun t1t2 => var1 (fst t1t2) * var2 (snd t1t2))%type (only parsing).
-      Local Notation eP := (fun t => var1 t * var2 t)%type (only parsing).
-      Local Notation "x == y" := (existT eP _ (x, y)).
-      Fixpoint flatten_binding_list2 {t1 t2} (x : interp_flat_type_gen var1 t1) (y : interp_flat_type_gen var2 t2) : list (sigT eP2)
-        := (match t1, t2 return interp_flat_type_gen var1 t1 -> interp_flat_type_gen var2 t2 -> list _ with
-            | Tbase t1, Tbase t2 => fun x y => existT eP2 (t1, t2)%core (x, y)%core :: nil
-            | Unit, Unit => fun x y => nil
-            | Prod t0 t1, Prod t0' t1'
-              => fun x y => @flatten_binding_list2 _ _ (snd x) (snd y) ++ @flatten_binding_list2 _ _ (fst x) (fst y)
-            | Tbase _, _
-            | Unit, _
-            | Prod _ _, _
-              => fun _ _ => nil
-            end x y)%list.
-      Fixpoint flatten_binding_list {t} (x : interp_flat_type_gen var1 t) (y : interp_flat_type_gen var2 t) : list (sigT eP)
-        := (match t return interp_flat_type_gen var1 t -> interp_flat_type_gen var2 t -> list _ with
-            | Tbase _ => fun x y => (x == y) :: nil
-            | Unit => fun x y => nil
-            | Prod t0 t1 => fun x y => @flatten_binding_list _ (snd x) (snd y) ++ @flatten_binding_list _ (fst x) (fst y)
-            end x y)%list.
-
-      Inductive wff : list (sigT eP) -> forall {t}, @exprf var1 t -> @exprf var2 t -> Prop :=
-      | WfTT : forall G, @wff G _ TT TT
-      | WfVar : forall G (t : base_type_code) x x', List.In (x == x') G -> @wff G t (Var x) (Var x')
-      | WfOp : forall G {t} {tR} (e : @exprf var1 t) (e' : @exprf var2 t) op,
-          wff G e e'
-          -> wff G (Op (tR := tR) op e) (Op (tR := tR) op e')
-      | WfLetIn : forall G t1 t2 e1 e1' (e2 : interp_flat_type_gen var1 t1 -> @exprf var1 t2) e2',
-          wff G e1 e1'
-          -> (forall x1 x2, wff (flatten_binding_list x1 x2 ++ G) (e2 x1) (e2' x2))
-          -> wff G (LetIn e1 e2) (LetIn e1' e2')
-      | WfPair : forall G {t1} {t2} (e1: @exprf var1 t1) (e2: @exprf var1 t2)
-                        (e1': @exprf var2 t1) (e2': @exprf var2 t2),
-          wff G e1 e1'
-          -> wff G e2 e2'
-          -> wff G (Pair e1 e2) (Pair e1' e2').
-      Inductive wf : list (sigT eP) -> forall {t}, @expr var1 t -> @expr var2 t -> Prop :=
-      | WfReturn : forall t G e e', @wff G t e e' -> wf G (Return e) (Return e')
-      | WfAbs : forall A B G e e',
-          (forall x x', @wf ((x == x') :: G) B (e x) (e' x'))
-          -> @wf G (Arrow A B) (Abs e) (Abs e').
-    End wf.
-
-    Definition Wf {t} (E : @Expr t) := forall var1 var2, wf nil (E var1) (E var2).
-
-    Axiom Wf_admitted : forall {t} (E:Expr t), @Wf t E.
   End expr_param.
 End language.
 Global Arguments tuple' {_}%type_scope _%ctype_scope _%nat_scope.
@@ -357,87 +125,21 @@ Global Arguments Arrow {_}%type_scope (_ _)%ctype_scope.
 Global Arguments Tbase {_}%type_scope _%ctype_scope.
 Global Arguments Tflat {_}%type_scope _%ctype_scope.
 
-Ltac admit_Wf := apply Wf_admitted.
-
 Global Arguments Var {_ _ _ _} _.
-Global Arguments SmartVarf {_ _ _ _} _.
-Global Arguments SmartPairf {_ _ _ t} _.
-Global Arguments SmartValf {_} T _ t.
-Global Arguments SmartVarVarf {_ _ _ _} _.
-Global Arguments SmartVarfMap {_ _ _} _ {_} _.
-Global Arguments SmartVarfMap2 {_ _ _ _} _ {t} _ _.
-Global Arguments SmartVarfTypeMap {_ _} _ {_} _.
-Global Arguments SmartVarfPropMap {_ _} _ {_} _.
-Global Arguments SmartVarfTypeMap2 {_ _ _} _ {t} _ _.
-Global Arguments SmartVarfPropMap2 {_ _ _} _ {t} _ _.
-Global Arguments SmartFlatTypeMap {_ _} _ {_} _.
-Global Arguments SmartFlatTypeUnMap {_} _ : assert.
-Global Arguments SmartFlatTypeMapInterp {_ _ _ _} _ {_} _.
-Global Arguments SmartFlatTypeMapUnInterp {_ _ _ _ _} fv {_ _} _.
-Global Arguments SmartVarMap_hetero {_ _ _ _ _} _ _ {_} _.
-Global Arguments SmartVarMap {_ _ _} _ _ {_} _.
-(*Global Arguments SmartConstf {_ _ _ _ _} _.*)
 Global Arguments TT {_ _ _}.
 Global Arguments Op {_ _ _ _ _} _ _.
 Global Arguments LetIn {_ _ _ _} _ {_} _.
 Global Arguments Pair {_ _ _ _} _ {_} _.
 Global Arguments Return {_ _ _ _} _.
 Global Arguments Abs {_ _ _ _ _} _.
-Global Arguments SmartAbs {_ _ _ _ _} _.
-Global Arguments mapf_interp_flat_type {_ _ _} _ {t} _.
 Global Arguments interp_type_gen_hetero {_} _ _ _.
 Global Arguments interp_type_gen {_} _ _.
 Global Arguments interp_flat_type {_} _ _.
 Global Arguments interp_type {_} _ _.
-Global Arguments wff {_ _ _ _} G {t} _ _.
-Global Arguments wf {_ _ _ _} G {t} _ _.
-Global Arguments Wf {_ _ t} _.
 Global Arguments Interp {_ _ _} interp_op {t} _.
 Global Arguments interp {_ _ _} interp_op {t} _.
 Global Arguments interpf {_ _ _} interp_op {t} _.
 
-Section hetero_type.
-  Fixpoint flatten_flat_type {base_type_code} (t : flat_type (flat_type base_type_code)) : flat_type base_type_code
-    := match t with
-       | Tbase T => T
-       | Unit => Unit
-       | Prod A B => Prod (@flatten_flat_type _ A) (@flatten_flat_type _ B)
-       end.
-
-  Section smart_flat_type_map2.
-    Context {base_type_code1 base_type_code2 : Type}.
-
-    Definition SmartFlatTypeMap2 {var' : base_type_code1 -> Type} (f : forall t, var' t -> flat_type base_type_code2) {t}
-      : interp_flat_type var' t -> flat_type base_type_code2
-      := @smart_interp_flat_map base_type_code1 var' (fun _ => flat_type base_type_code2) f Unit (fun _ _ => Prod) t.
-    Fixpoint SmartFlatTypeMapInterp2 {var' var''} (f : forall t, var' t -> flat_type base_type_code2)
-             (fv : forall t v, interp_flat_type var'' (f t v)) t {struct t}
-      : forall v, interp_flat_type var'' (SmartFlatTypeMap2 f (t:=t) v)
-      := match t return forall v, interp_flat_type var'' (SmartFlatTypeMap2 f (t:=t) v) with
-         | Tbase x => fv _
-         | Unit => fun v => v
-         | Prod A B => fun xy => (@SmartFlatTypeMapInterp2 _ _ f fv A (fst xy),
-                                  @SmartFlatTypeMapInterp2 _ _ f fv B (snd xy))
-         end.
-    Fixpoint SmartFlatTypeMapUnInterp2 var' var'' var''' (f : forall t, var' t -> flat_type base_type_code2)
-             (fv : forall t (v : var' t), interp_flat_type var'' (f t v) -> var''' t)
-             {t} {struct t}
-      : forall v, interp_flat_type var'' (SmartFlatTypeMap2 f (t:=t) v)
-                  -> interp_flat_type var''' t
-      := match t return forall v, interp_flat_type var'' (SmartFlatTypeMap2 f (t:=t) v)
-                                  -> interp_flat_type var''' t with
-         | Tbase x => fv _
-         | Unit => fun _ v => v
-         | Prod A B => fun v xy => (@SmartFlatTypeMapUnInterp2 _ _ _ f fv A _ (fst xy),
-                                    @SmartFlatTypeMapUnInterp2 _ _ _ f fv B _ (snd xy))
-         end.
-  End smart_flat_type_map2.
-End hetero_type.
-
-Global Arguments SmartFlatTypeMap2 {_ _ _} _ {_} _.
-Global Arguments SmartFlatTypeMapInterp2 {_ _ _ _ _} _ {_} _.
-Global Arguments SmartFlatTypeMapUnInterp2 {_ _ _ _ _ _} fv {_ _} _.
-
 Module Export Notations.
   Notation "()" := (@Unit _) : ctype_scope.
   Notation "A * B" := (@Prod _ A B) : ctype_scope.
diff --git a/src/Reflection/TestCase.v b/src/Reflection/TestCase.v
index 2d70dfd3e..c4287239e 100644
--- a/src/Reflection/TestCase.v
+++ b/src/Reflection/TestCase.v
@@ -4,6 +4,7 @@ Require Import Crypto.Reflection.Named.Syntax.
 Require Import Crypto.Reflection.Named.Compile.
 Require Import Crypto.Reflection.Named.RegisterAssign.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.Equality.
 Require Export Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.InputSyntax.
diff --git a/src/Reflection/Wf.v b/src/Reflection/Wf.v
new file mode 100644
index 000000000..21bedf6b3
--- /dev/null
+++ b/src/Reflection/Wf.v
@@ -0,0 +1,67 @@
+Require Import Coq.Lists.List.
+Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Util.Notations.
+
+Section language.
+  Context {base_type_code : Type}
+          {op : flat_type base_type_code -> flat_type base_type_code -> Type}.
+  Local Notation exprf := (@exprf base_type_code op).
+  Local Notation expr := (@expr base_type_code op).
+  Local Notation Expr := (@Expr base_type_code op).
+
+  Section with_var.
+    Context {var1 var2 : base_type_code -> Type}.
+
+    Local Notation eP2 := (fun t1t2 => var1 (fst t1t2) * var2 (snd t1t2))%type (only parsing).
+    Local Notation eP := (fun t => var1 t * var2 t)%type (only parsing).
+    Local Notation "x == y" := (existT eP _ (x, y)%core).
+    Fixpoint flatten_binding_list2 {t1 t2} (x : interp_flat_type var1 t1) (y : interp_flat_type var2 t2) : list (sigT eP2)
+      := (match t1, t2 return interp_flat_type var1 t1 -> interp_flat_type var2 t2 -> list _ with
+          | Tbase t1, Tbase t2 => fun x y => existT eP2 (t1, t2)%core (x, y)%core :: nil
+          | Unit, Unit => fun x y => nil
+          | Prod t0 t1, Prod t0' t1'
+            => fun x y => @flatten_binding_list2 _ _ (snd x) (snd y) ++ @flatten_binding_list2 _ _ (fst x) (fst y)
+          | Tbase _, _
+          | Unit, _
+          | Prod _ _, _
+            => fun _ _ => nil
+          end x y)%list.
+    Fixpoint flatten_binding_list {t} (x : interp_flat_type var1 t) (y : interp_flat_type var2 t) : list (sigT eP)
+      := (match t return interp_flat_type var1 t -> interp_flat_type var2 t -> list _ with
+          | Tbase _ => fun x y => (x == y) :: nil
+          | Unit => fun x y => nil
+          | Prod t0 t1 => fun x y => @flatten_binding_list _ (snd x) (snd y) ++ @flatten_binding_list _ (fst x) (fst y)
+          end x y)%list.
+
+    Inductive wff : list (sigT eP) -> forall {t}, @exprf var1 t -> @exprf var2 t -> Prop :=
+    | WfTT : forall G, @wff G _ TT TT
+    | WfVar : forall G (t : base_type_code) x x', List.In (x == x') G -> @wff G (Tbase t) (Var x) (Var x')
+    | WfOp : forall G {t} {tR} (e : @exprf var1 t) (e' : @exprf var2 t) op,
+        wff G e e'
+        -> wff G (Op (tR := tR) op e) (Op (tR := tR) op e')
+    | WfLetIn : forall G t1 t2 e1 e1' (e2 : interp_flat_type var1 t1 -> @exprf var1 t2) e2',
+        wff G e1 e1'
+        -> (forall x1 x2, wff (flatten_binding_list x1 x2 ++ G) (e2 x1) (e2' x2))
+        -> wff G (LetIn e1 e2) (LetIn e1' e2')
+    | WfPair : forall G {t1} {t2} (e1: @exprf var1 t1) (e2: @exprf var1 t2)
+                      (e1': @exprf var2 t1) (e2': @exprf var2 t2),
+        wff G e1 e1'
+        -> wff G e2 e2'
+        -> wff G (Pair e1 e2) (Pair e1' e2').
+    Inductive wf : list (sigT eP) -> forall {t}, @expr var1 t -> @expr var2 t -> Prop :=
+    | WfReturn : forall t G e e', @wff G t e e' -> wf G (Return e) (Return e')
+    | WfAbs : forall A B G e e',
+        (forall x x', @wf ((x == x') :: G) B (e x) (e' x'))
+        -> @wf G (Arrow A B) (Abs e) (Abs e').
+  End with_var.
+
+  Definition Wf {t} (E : @Expr t) := forall var1 var2, wf nil (E var1) (E var2).
+
+  Axiom Wf_admitted : forall {t} (E:Expr t), @Wf t E.
+End language.
+
+Ltac admit_Wf := apply Wf_admitted.
+
+Global Arguments wff {_ _ _ _} G {t} _ _.
+Global Arguments wf {_ _ _ _} G {t} _ _.
+Global Arguments Wf {_ _ t} _.
diff --git a/src/Reflection/WfInversion.v b/src/Reflection/WfInversion.v
index 4a253f28b..bf396d52e 100644
--- a/src/Reflection/WfInversion.v
+++ b/src/Reflection/WfInversion.v
@@ -1,4 +1,5 @@
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Util.Sigma.
 Require Import Crypto.Util.Option.
@@ -52,7 +53,7 @@ Section language.
                    => { pf : tx1 = tx2
                       | wff G (eq_rect _ exprf ex1 _ pf) ex2
                         /\ (forall x1 x2,
-                               wff (flatten_binding_list base_type_code x1 x2 ++ G)%list
+                               wff (flatten_binding_list x1 x2 ++ G)%list
                                    (eC1 x1) (eC2 (eq_rect _ _ x2 _ pf))) }
                  | None => False
                  end
diff --git a/src/Reflection/WfProofs.v b/src/Reflection/WfProofs.v
index 8b855c08f..66002e7d0 100644
--- a/src/Reflection/WfProofs.v
+++ b/src/Reflection/WfProofs.v
@@ -1,4 +1,6 @@
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Util.Tactics Crypto.Util.Sigma Crypto.Util.Prod.
 
@@ -16,7 +18,7 @@ Section language.
 
   Section with_var.
     Context {var1 var2 : base_type_code -> Type}.
-    Local Hint Constructors Syntax.wff.
+    Local Hint Constructors Wf.wff.
 
     Lemma wff_app' {g G0 G1 t e1 e2}
           (wf : @wff var1 var2 (G0 ++ G1) t e1 e2)
@@ -67,7 +69,7 @@ Section language.
     Local Hint Resolve wff_in_impl_Proper.
 
     Lemma wff_SmartVarf {t} x1 x2
-      : @wff var1 var2 (flatten_binding_list base_type_code x1 x2) t (SmartVarf x1) (SmartVarf x2).
+      : @wff var1 var2 (flatten_binding_list x1 x2) t (SmartVarf x1) (SmartVarf x2).
     Proof.
       unfold SmartVarf.
       induction t; simpl; constructor; eauto.
@@ -77,8 +79,8 @@ Section language.
 
     Lemma wff_SmartVarVarf G {t t'} v1 v2 x1 x2
           (Hin : List.In (existT (fun t : base_type_code => (exprf (Tbase t) * exprf (Tbase t))%type) t (x1, x2))
-                          (flatten_binding_list base_type_code (SmartVarVarf v1) (SmartVarVarf v2)))
-      : @wff var1 var2 (flatten_binding_list base_type_code (t:=t') v1 v2 ++ G) (Tbase t) x1 x2.
+                          (flatten_binding_list (SmartVarVarf v1) (SmartVarVarf v2)))
+      : @wff var1 var2 (flatten_binding_list (t:=t') v1 v2 ++ G) (Tbase t) x1 x2.
     Proof.
       revert dependent G; induction t'; intros; simpl in *; try tauto.
       { intuition (inversion_sigma; inversion_prod; subst; simpl; eauto).
@@ -119,51 +121,51 @@ Section language.
 
   Lemma flatten_binding_list2_SmartVarfMap
         {var1 var1' var2 var2' t1 t2} f g (x1 : interp_flat_type var1 t1) (x2 : interp_flat_type var2 t2)
-    : flatten_binding_list2 (var1:=var1') (var2:=var2') base_type_code (SmartVarfMap f x1) (SmartVarfMap g x2)
+    : flatten_binding_list2 (var1:=var1') (var2:=var2') (base_type_code:=base_type_code) (SmartVarfMap f x1) (SmartVarfMap g x2)
       = List.map (fun txy => existT _ (projT1 txy) (f _ (fst (projT2 txy)), g _ (snd (projT2 txy)))%core)
-                 (flatten_binding_list2 base_type_code x1 x2).
+                 (flatten_binding_list2 x1 x2).
   Proof.
     revert dependent t2; induction t1, t2; flatten_t.
   Qed.
 
   Lemma flatten_binding_list2_SmartVarfMap1
         {var1 var1' var2' t1 t2} f (x1 : interp_flat_type var1 t1) (x2 : interp_flat_type var2' t2)
-    : flatten_binding_list2 (var1:=var1') (var2:=var2') base_type_code (SmartVarfMap f x1) x2
+    : flatten_binding_list2 (var1:=var1') (var2:=var2') (base_type_code:=base_type_code) (SmartVarfMap f x1) x2
       = List.map (fun txy => existT _ (projT1 txy) (f _ (fst (projT2 txy)), snd (projT2 txy))%core)
-                 (flatten_binding_list2 base_type_code x1 x2).
+                 (flatten_binding_list2 x1 x2).
   Proof.
     revert dependent t2; induction t1, t2; flatten_t.
   Qed.
 
   Lemma flatten_binding_list2_SmartVarfMap2
         {var1' var2 var2' t1 t2} g (x1 : interp_flat_type var1' t1) (x2 : interp_flat_type var2 t2)
-    : flatten_binding_list2 (var1:=var1') (var2:=var2') base_type_code x1 (SmartVarfMap g x2)
+    : flatten_binding_list2 (var1:=var1') (var2:=var2') (base_type_code:=base_type_code) x1 (SmartVarfMap g x2)
       = List.map (fun txy => existT _ (projT1 txy) (fst (projT2 txy), g _ (snd (projT2 txy)))%core)
-                 (flatten_binding_list2 base_type_code x1 x2).
+                 (flatten_binding_list2 x1 x2).
   Proof.
     revert dependent t2; induction t1, t2; flatten_t.
   Qed.
 
   Lemma flatten_binding_list_SmartVarfMap
         {var1 var1' var2 var2' t} f g (x1 : interp_flat_type var1 t) (x2 : interp_flat_type var2 t)
-    : flatten_binding_list (var1:=var1') (var2:=var2') base_type_code (SmartVarfMap f x1) (SmartVarfMap g x2)
+    : flatten_binding_list (var1:=var1') (var2:=var2') (base_type_code:=base_type_code) (SmartVarfMap f x1) (SmartVarfMap g x2)
       = List.map (fun txy => existT _ (projT1 txy) (f _ (fst (projT2 txy)), g _ (snd (projT2 txy)))%core)
-                 (flatten_binding_list base_type_code x1 x2).
+                 (flatten_binding_list x1 x2).
   Proof. induction t; flatten_t. Qed.
 
   Lemma flatten_binding_list2_SmartValf
         {T1 T2} f g t1 t2
-    : flatten_binding_list2 base_type_code (SmartValf T1 f t1) (SmartValf T2 g t2)
+    : flatten_binding_list2 (base_type_code:=base_type_code) (SmartValf T1 f t1) (SmartValf T2 g t2)
       = List.map (fun txy => existT _ (projT1 txy) (f _, g _)%core)
-                 (flatten_binding_list2 base_type_code (SmartFlatTypeUnMap t1) (SmartFlatTypeUnMap t2)).
+                 (flatten_binding_list2 (SmartFlatTypeUnMap t1) (SmartFlatTypeUnMap t2)).
   Proof.
     revert dependent t2; induction t1, t2; flatten_t.
   Qed.
 
   Lemma flatten_binding_list_SmartValf
         {T1 T2} f g t
-    : flatten_binding_list base_type_code (SmartValf T1 f t) (SmartValf T2 g t)
+    : flatten_binding_list (base_type_code:=base_type_code) (SmartValf T1 f t) (SmartValf T2 g t)
       = List.map (fun txy => existT _ (projT1 txy) (f _, g _)%core)
-                 (flatten_binding_list base_type_code (SmartFlatTypeUnMap t) (SmartFlatTypeUnMap t)).
+                 (flatten_binding_list (SmartFlatTypeUnMap t) (SmartFlatTypeUnMap t)).
   Proof. induction t; flatten_t. Qed.
 End language.
diff --git a/src/Reflection/WfReflective.v b/src/Reflection/WfReflective.v
index 88e6bf5b0..da731d511 100644
--- a/src/Reflection/WfReflective.v
+++ b/src/Reflection/WfReflective.v
@@ -49,6 +49,7 @@
 
 Require Import Coq.Arith.Arith Coq.Logic.Eqdep_dec.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.WfReflectiveGen.
 Require Import Crypto.Util.Notations Crypto.Util.Tactics Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable Crypto.Util.ListUtil.
 Require Export Crypto.Util.PartiallyReifiedProp. (* export for the [bool >-> reified_Prop] coercion *)
@@ -114,7 +115,7 @@ Section language.
     | [ v : ex _ |- _ ] => destruct v
     | [ v : sigT _ |- _ ] => destruct v
     | [ v : prod _ _ |- _ ] => destruct v
-    | [ H : forall x x', _ |- wff (flatten_binding_list _ ?x1 ?x2 ++ _)%list _ _ ]
+    | [ H : forall x x', _ |- wff (flatten_binding_list ?x1 ?x2 ++ _)%list _ _ ]
       => specialize (H x1 x2)
     | [ H : forall x x', _ |- wf (existT _ _ (?x1, ?x2) :: _)%list _ _ ]
       => specialize (H x1 x2)
diff --git a/src/Reflection/WfReflectiveGen.v b/src/Reflection/WfReflectiveGen.v
index a562531c3..d4c0b45d0 100644
--- a/src/Reflection/WfReflectiveGen.v
+++ b/src/Reflection/WfReflectiveGen.v
@@ -50,6 +50,7 @@
 Require Import Coq.Arith.Arith Coq.Logic.Eqdep_dec.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Util.Notations Crypto.Util.Tactics Crypto.Util.Option Crypto.Util.Sigma Crypto.Util.Prod Crypto.Util.Decidable Crypto.Util.ListUtil.
+Require Import Crypto.Reflection.Wf.
 Require Export Crypto.Util.PartiallyReifiedProp. (* export for the [bool >-> reified_Prop] coercion *)
 Require Export Crypto.Util.FixCoqMistakes.
 
@@ -219,7 +220,7 @@ Section language.
        | Some p
          => Some (fun x y
                  => let x := eq_rect _ (interp_flat_type var1) x _ p in
-                   flatten_binding_list base_type_code x y)
+                   flatten_binding_list x y)
        | None => None
        end.
   Definition flatten_binding_list2 t1 t2 : option (forall (x : interp_flat_type var1 t1) (y : interp_flat_type var2 t2), list (sigT eP))
@@ -240,14 +241,14 @@ Section language.
        end v.
   Arguments natize_interp_flat_type {var t} _ _.
   Lemma length_natize_interp_flat_type1 {t} (base : nat) (v1 : interp_flat_type var1 t) (v2 : interp_flat_type var2 t)
-    : fst (natize_interp_flat_type base v1) = length (flatten_binding_list base_type_code v1 v2) + base.
+    : fst (natize_interp_flat_type base v1) = length (flatten_binding_list v1 v2) + base.
   Proof.
     revert base; induction t; simpl; [ reflexivity | reflexivity | ].
     intros; rewrite List.app_length, <- plus_assoc.
     rewrite_hyp <- ?*; reflexivity.
   Qed.
   Lemma length_natize_interp_flat_type2 {t} (base : nat) (v1 : interp_flat_type var1 t) (v2 : interp_flat_type var2 t)
-    : fst (natize_interp_flat_type base v2) = length (flatten_binding_list base_type_code v1 v2) + base.
+    : fst (natize_interp_flat_type base v2) = length (flatten_binding_list v1 v2) + base.
   Proof.
     revert base; induction t; simpl; [ reflexivity | reflexivity | ].
     intros; rewrite List.app_length, <- plus_assoc.
diff --git a/src/Reflection/Z/Interpretations128/Relations.v b/src/Reflection/Z/Interpretations128/Relations.v
index fcd7bf2d8..2a7db515a 100644
--- a/src/Reflection/Z/Interpretations128/Relations.v
+++ b/src/Reflection/Z/Interpretations128/Relations.v
@@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Psatz.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Tuple.
 Require Import Crypto.Reflection.Z.InterpretationsGen.
diff --git a/src/Reflection/Z/Interpretations128/RelationsCombinations.v b/src/Reflection/Z/Interpretations128/RelationsCombinations.v
index 2de4510c7..d5c07513d 100644
--- a/src/Reflection/Z/Interpretations128/RelationsCombinations.v
+++ b/src/Reflection/Z/Interpretations128/RelationsCombinations.v
@@ -1,6 +1,7 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.Z.InterpretationsGen.
diff --git a/src/Reflection/Z/Interpretations64/Relations.v b/src/Reflection/Z/Interpretations64/Relations.v
index 6b4279043..525ecd266 100644
--- a/src/Reflection/Z/Interpretations64/Relations.v
+++ b/src/Reflection/Z/Interpretations64/Relations.v
@@ -2,6 +2,7 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.micromega.Psatz.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Tuple.
 Require Import Crypto.Reflection.Z.InterpretationsGen.
diff --git a/src/Reflection/Z/Interpretations64/RelationsCombinations.v b/src/Reflection/Z/Interpretations64/RelationsCombinations.v
index 8777cd7ed..d4a125499 100644
--- a/src/Reflection/Z/Interpretations64/RelationsCombinations.v
+++ b/src/Reflection/Z/Interpretations64/RelationsCombinations.v
@@ -1,6 +1,7 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Reflection.Z.InterpretationsGen.
diff --git a/src/Reflection/Z/InterpretationsGen.v b/src/Reflection/Z/InterpretationsGen.v
index 3b403acc8..6ccb23960 100644
--- a/src/Reflection/Z/InterpretationsGen.v
+++ b/src/Reflection/Z/InterpretationsGen.v
@@ -2,6 +2,7 @@
 Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.ModularArithmetic.ModularBaseSystemListZOperations.
 Require Import Crypto.Util.Equality.
diff --git a/src/Specific/GF25519Reflective.v b/src/Specific/GF25519Reflective.v
index dd4545094..e2b26016d 100644
--- a/src/Specific/GF25519Reflective.v
+++ b/src/Specific/GF25519Reflective.v
@@ -9,6 +9,7 @@ Require Export Crypto.Specific.GF25519.
 Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
diff --git a/src/Specific/GF25519Reflective/Common.v b/src/Specific/GF25519Reflective/Common.v
index d47e71933..263edf3fe 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.SmartMap.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.
@@ -43,7 +45,7 @@ Definition Expr_n_OpT (count_out : nat) : flat_type base_type
 Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type
   := match count_in with
      | 0 => Expr_n_OpT count_out
-     | S n => SmartArrow base_type fe25519T (Expr_nm_OpT n count_out)
+     | S n => SmartArrow fe25519T (Expr_nm_OpT n count_out)
      end.
 Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1.
 Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1.
diff --git a/src/Specific/GF25519Reflective/Common9_4Op.v b/src/Specific/GF25519Reflective/Common9_4Op.v
index 5fbb72c26..2d0f2d2cb 100644
--- a/src/Specific/GF25519Reflective/Common9_4Op.v
+++ b/src/Specific/GF25519Reflective/Common9_4Op.v
@@ -2,6 +2,7 @@ Require Export Crypto.Specific.GF25519Reflective.Common.
 Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/Specific/GF25519Reflective/CommonBinOp.v b/src/Specific/GF25519Reflective/CommonBinOp.v
index 07c0d82dd..f3f8d4482 100644
--- a/src/Specific/GF25519Reflective/CommonBinOp.v
+++ b/src/Specific/GF25519Reflective/CommonBinOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.Specific.GF25519Reflective.Common.
 Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/Specific/GF25519Reflective/CommonUnOp.v b/src/Specific/GF25519Reflective/CommonUnOp.v
index a55bdc58d..6d67170a4 100644
--- a/src/Specific/GF25519Reflective/CommonUnOp.v
+++ b/src/Specific/GF25519Reflective/CommonUnOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.Specific.GF25519Reflective.Common.
 Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v b/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v
index b9395d3ef..fc3fa5a63 100644
--- a/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v
+++ b/src/Specific/GF25519Reflective/CommonUnOpFEToWire.v
@@ -2,6 +2,7 @@ Require Export Crypto.Specific.GF25519Reflective.Common.
 Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v b/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v
index 55ce98a40..f112184e9 100644
--- a/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v
+++ b/src/Specific/GF25519Reflective/CommonUnOpFEToZ.v
@@ -2,6 +2,7 @@ Require Export Crypto.Specific.GF25519Reflective.Common.
 Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v b/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v
index 023969413..0ba44ecc9 100644
--- a/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v
+++ b/src/Specific/GF25519Reflective/CommonUnOpWireToFE.v
@@ -2,6 +2,7 @@ Require Export Crypto.Specific.GF25519Reflective.Common.
 Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v
index c80aa7ffa..d35a0e5e9 100644
--- a/src/Specific/GF25519Reflective/Reified/AddCoordinates.v
+++ b/src/Specific/GF25519Reflective/Reified/AddCoordinates.v
@@ -4,6 +4,7 @@ Require Export Crypto.Specific.GF25519.
 Require Export Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Application.
diff --git a/src/Specific/GF25519Reflective/Reified/LadderStep.v b/src/Specific/GF25519Reflective/Reified/LadderStep.v
index d888197f2..d82ac17ae 100644
--- a/src/Specific/GF25519Reflective/Reified/LadderStep.v
+++ b/src/Specific/GF25519Reflective/Reified/LadderStep.v
@@ -4,6 +4,7 @@ Require Export Crypto.Specific.GF25519.
 Require Export Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Application.
diff --git a/src/Specific/GF25519ReflectiveAddCoordinates.v b/src/Specific/GF25519ReflectiveAddCoordinates.v
index 955957a11..c4e88f2a7 100644
--- a/src/Specific/GF25519ReflectiveAddCoordinates.v
+++ b/src/Specific/GF25519ReflectiveAddCoordinates.v
@@ -9,6 +9,7 @@ Require Export Crypto.Specific.GF25519.
 Require Import Crypto.Specific.GF25519BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
diff --git a/src/SpecificGen/GF2213_32Reflective.v b/src/SpecificGen/GF2213_32Reflective.v
index 2f43e92fd..078dc2c4a 100644
--- a/src/SpecificGen/GF2213_32Reflective.v
+++ b/src/SpecificGen/GF2213_32Reflective.v
@@ -9,6 +9,7 @@ Require Export Crypto.SpecificGen.GF2213_32.
 Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
diff --git a/src/SpecificGen/GF2213_32Reflective/Common.v b/src/SpecificGen/GF2213_32Reflective/Common.v
index 977f47e69..8c21298a2 100644
--- a/src/SpecificGen/GF2213_32Reflective/Common.v
+++ b/src/SpecificGen/GF2213_32Reflective/Common.v
@@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2213_32.
 Require Export Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.
@@ -43,7 +45,7 @@ Definition Expr_n_OpT (count_out : nat) : flat_type base_type
 Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type
   := match count_in with
      | 0 => Expr_n_OpT count_out
-     | S n => SmartArrow base_type fe2213_32T (Expr_nm_OpT n count_out)
+     | S n => SmartArrow fe2213_32T (Expr_nm_OpT n count_out)
      end.
 Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1.
 Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1.
diff --git a/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v b/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v
index 49a4782eb..fb8b27f18 100644
--- a/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v
+++ b/src/SpecificGen/GF2213_32Reflective/Common9_4Op.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF2213_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v b/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v
index 0cdef8deb..8ad7f623c 100644
--- a/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v
+++ b/src/SpecificGen/GF2213_32Reflective/CommonBinOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF2213_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v
index 5df7f6c98..40b39edf4 100644
--- a/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v
+++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF2213_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v
index 0751754d7..60c0726dc 100644
--- a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v
+++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToWire.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF2213_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v
index d6cf8653d..bc5a6e265 100644
--- a/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v
+++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOpFEToZ.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF2213_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v
index 15dc52517..e4f57d7bb 100644
--- a/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v
+++ b/src/SpecificGen/GF2213_32Reflective/CommonUnOpWireToFE.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF2213_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v
index c2fb547d0..a51afcf06 100644
--- a/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/AddCoordinates.v
@@ -4,6 +4,7 @@ Require Export Crypto.SpecificGen.GF2213_32.
 Require Export Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Application.
diff --git a/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v
index 51b07c4d6..1ac755508 100644
--- a/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v
+++ b/src/SpecificGen/GF2213_32Reflective/Reified/LadderStep.v
@@ -4,6 +4,7 @@ Require Export Crypto.SpecificGen.GF2213_32.
 Require Export Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Application.
diff --git a/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v
index 4dd4b8e9e..aaf0c2833 100644
--- a/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v
+++ b/src/SpecificGen/GF2213_32ReflectiveAddCoordinates.v
@@ -9,6 +9,7 @@ Require Export Crypto.SpecificGen.GF2213_32.
 Require Import Crypto.SpecificGen.GF2213_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
diff --git a/src/SpecificGen/GF2519_32Reflective.v b/src/SpecificGen/GF2519_32Reflective.v
index f3c1d7c08..6b912c7ea 100644
--- a/src/SpecificGen/GF2519_32Reflective.v
+++ b/src/SpecificGen/GF2519_32Reflective.v
@@ -9,6 +9,7 @@ Require Export Crypto.SpecificGen.GF2519_32.
 Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
diff --git a/src/SpecificGen/GF2519_32Reflective/Common.v b/src/SpecificGen/GF2519_32Reflective/Common.v
index 6f6f607fb..31c3944c8 100644
--- a/src/SpecificGen/GF2519_32Reflective/Common.v
+++ b/src/SpecificGen/GF2519_32Reflective/Common.v
@@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF2519_32.
 Require Export Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.
@@ -43,7 +45,7 @@ Definition Expr_n_OpT (count_out : nat) : flat_type base_type
 Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type
   := match count_in with
      | 0 => Expr_n_OpT count_out
-     | S n => SmartArrow base_type fe2519_32T (Expr_nm_OpT n count_out)
+     | S n => SmartArrow fe2519_32T (Expr_nm_OpT n count_out)
      end.
 Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1.
 Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1.
diff --git a/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v b/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v
index 6a07ae3cf..990ad0e53 100644
--- a/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v
+++ b/src/SpecificGen/GF2519_32Reflective/Common9_4Op.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v b/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v
index e20ab88d1..c0c390d0b 100644
--- a/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v
+++ b/src/SpecificGen/GF2519_32Reflective/CommonBinOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v
index 505a9a9ce..b2117295a 100644
--- a/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v
+++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v
index e84df9be2..1b20ac0f5 100644
--- a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v
+++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToWire.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v
index 054155d1f..dc49c8ec8 100644
--- a/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v
+++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOpFEToZ.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v
index b22e73f6e..b500e4cb0 100644
--- a/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v
+++ b/src/SpecificGen/GF2519_32Reflective/CommonUnOpWireToFE.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF2519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v
index 1e74a8cf5..5033de383 100644
--- a/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF2519_32Reflective/Reified/AddCoordinates.v
@@ -4,6 +4,7 @@ Require Export Crypto.SpecificGen.GF2519_32.
 Require Export Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Application.
diff --git a/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v
index 3a069c45c..c06a2cb59 100644
--- a/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v
+++ b/src/SpecificGen/GF2519_32Reflective/Reified/LadderStep.v
@@ -4,6 +4,7 @@ Require Export Crypto.SpecificGen.GF2519_32.
 Require Export Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Application.
diff --git a/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v
index e1f691607..3ceccc8dd 100644
--- a/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v
+++ b/src/SpecificGen/GF2519_32ReflectiveAddCoordinates.v
@@ -9,6 +9,7 @@ Require Export Crypto.SpecificGen.GF2519_32.
 Require Import Crypto.SpecificGen.GF2519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
diff --git a/src/SpecificGen/GF25519_32Reflective.v b/src/SpecificGen/GF25519_32Reflective.v
index d3e45d36d..cfa76bf01 100644
--- a/src/SpecificGen/GF25519_32Reflective.v
+++ b/src/SpecificGen/GF25519_32Reflective.v
@@ -9,6 +9,7 @@ Require Export Crypto.SpecificGen.GF25519_32.
 Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
diff --git a/src/SpecificGen/GF25519_32Reflective/Common.v b/src/SpecificGen/GF25519_32Reflective/Common.v
index bd01c31a2..017a7480a 100644
--- a/src/SpecificGen/GF25519_32Reflective/Common.v
+++ b/src/SpecificGen/GF25519_32Reflective/Common.v
@@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_32.
 Require Export Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.
@@ -43,7 +45,7 @@ Definition Expr_n_OpT (count_out : nat) : flat_type base_type
 Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type
   := match count_in with
      | 0 => Expr_n_OpT count_out
-     | S n => SmartArrow base_type fe25519_32T (Expr_nm_OpT n count_out)
+     | S n => SmartArrow fe25519_32T (Expr_nm_OpT n count_out)
      end.
 Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1.
 Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1.
diff --git a/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v b/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v
index fc0bf3d0b..286724558 100644
--- a/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v
+++ b/src/SpecificGen/GF25519_32Reflective/Common9_4Op.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF25519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v b/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v
index 3053b6d51..6a8a54fdd 100644
--- a/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v
+++ b/src/SpecificGen/GF25519_32Reflective/CommonBinOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF25519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v
index dd7c392b1..8df0c1685 100644
--- a/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v
+++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF25519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v
index f05bfdba4..d97e1e8c9 100644
--- a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v
+++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToWire.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF25519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v
index ea8f01446..1a6f994e5 100644
--- a/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v
+++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOpFEToZ.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF25519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v
index 2a19f9eb1..62572dc0c 100644
--- a/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v
+++ b/src/SpecificGen/GF25519_32Reflective/CommonUnOpWireToFE.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF25519_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v
index c276df344..d5c05a6e5 100644
--- a/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF25519_32Reflective/Reified/AddCoordinates.v
@@ -4,6 +4,7 @@ Require Export Crypto.SpecificGen.GF25519_32.
 Require Export Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Application.
diff --git a/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v
index 33b232dc2..9f133bb39 100644
--- a/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v
+++ b/src/SpecificGen/GF25519_32Reflective/Reified/LadderStep.v
@@ -4,6 +4,7 @@ Require Export Crypto.SpecificGen.GF25519_32.
 Require Export Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Application.
diff --git a/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v
index b4840a4d2..1392cb2f6 100644
--- a/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v
+++ b/src/SpecificGen/GF25519_32ReflectiveAddCoordinates.v
@@ -9,6 +9,7 @@ Require Export Crypto.SpecificGen.GF25519_32.
 Require Import Crypto.SpecificGen.GF25519_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
diff --git a/src/SpecificGen/GF25519_64Reflective.v b/src/SpecificGen/GF25519_64Reflective.v
index 620c96713..b92c70202 100644
--- a/src/SpecificGen/GF25519_64Reflective.v
+++ b/src/SpecificGen/GF25519_64Reflective.v
@@ -9,6 +9,7 @@ Require Export Crypto.SpecificGen.GF25519_64.
 Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations128.
 Require Crypto.Reflection.Z.Interpretations128.Relations.
 Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations.
diff --git a/src/SpecificGen/GF25519_64Reflective/Common.v b/src/SpecificGen/GF25519_64Reflective/Common.v
index dd78063a8..ea24e8745 100644
--- a/src/SpecificGen/GF25519_64Reflective/Common.v
+++ b/src/SpecificGen/GF25519_64Reflective/Common.v
@@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF25519_64.
 Require Export Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Z.Interpretations128.
@@ -43,7 +45,7 @@ Definition Expr_n_OpT (count_out : nat) : flat_type base_type
 Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type
   := match count_in with
      | 0 => Expr_n_OpT count_out
-     | S n => SmartArrow base_type fe25519_64T (Expr_nm_OpT n count_out)
+     | S n => SmartArrow fe25519_64T (Expr_nm_OpT n count_out)
      end.
 Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1.
 Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1.
diff --git a/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v b/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v
index 9699d43b4..9435884a4 100644
--- a/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v
+++ b/src/SpecificGen/GF25519_64Reflective/Common9_4Op.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF25519_64Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations128.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v b/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v
index 5ebff74a9..1d174ae2b 100644
--- a/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v
+++ b/src/SpecificGen/GF25519_64Reflective/CommonBinOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF25519_64Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations128.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v
index 53b0c372f..a5b57d394 100644
--- a/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v
+++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF25519_64Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations128.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v
index b9c642d43..cdda3c4eb 100644
--- a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v
+++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToWire.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF25519_64Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations128.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v
index fcc07a651..d082f70b0 100644
--- a/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v
+++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOpFEToZ.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF25519_64Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations128.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v
index 09292ea2c..327a6b825 100644
--- a/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v
+++ b/src/SpecificGen/GF25519_64Reflective/CommonUnOpWireToFE.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF25519_64Reflective.Common.
 Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations128.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v
index a109ec89b..3303a53bb 100644
--- a/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF25519_64Reflective/Reified/AddCoordinates.v
@@ -4,6 +4,7 @@ Require Export Crypto.SpecificGen.GF25519_64.
 Require Export Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Application.
diff --git a/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v
index c105a2846..33dab7528 100644
--- a/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v
+++ b/src/SpecificGen/GF25519_64Reflective/Reified/LadderStep.v
@@ -4,6 +4,7 @@ Require Export Crypto.SpecificGen.GF25519_64.
 Require Export Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Application.
diff --git a/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v b/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v
index 9050ee849..2527f2c90 100644
--- a/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v
+++ b/src/SpecificGen/GF25519_64ReflectiveAddCoordinates.v
@@ -9,6 +9,7 @@ Require Export Crypto.SpecificGen.GF25519_64.
 Require Import Crypto.SpecificGen.GF25519_64BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations128.
 Require Crypto.Reflection.Z.Interpretations128.Relations.
 Require Import Crypto.Reflection.Z.Interpretations128.RelationsCombinations.
diff --git a/src/SpecificGen/GF41417_32Reflective.v b/src/SpecificGen/GF41417_32Reflective.v
index efc54565e..4b9b012b1 100644
--- a/src/SpecificGen/GF41417_32Reflective.v
+++ b/src/SpecificGen/GF41417_32Reflective.v
@@ -9,6 +9,7 @@ Require Export Crypto.SpecificGen.GF41417_32.
 Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
diff --git a/src/SpecificGen/GF41417_32Reflective/Common.v b/src/SpecificGen/GF41417_32Reflective/Common.v
index 9ab04a78f..5af82a994 100644
--- a/src/SpecificGen/GF41417_32Reflective/Common.v
+++ b/src/SpecificGen/GF41417_32Reflective/Common.v
@@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF41417_32.
 Require Export Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.
@@ -43,7 +45,7 @@ Definition Expr_n_OpT (count_out : nat) : flat_type base_type
 Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type
   := match count_in with
      | 0 => Expr_n_OpT count_out
-     | S n => SmartArrow base_type fe41417_32T (Expr_nm_OpT n count_out)
+     | S n => SmartArrow fe41417_32T (Expr_nm_OpT n count_out)
      end.
 Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1.
 Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1.
diff --git a/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v b/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v
index f1230b04e..4590d5871 100644
--- a/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v
+++ b/src/SpecificGen/GF41417_32Reflective/Common9_4Op.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF41417_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v b/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v
index 438110cb8..d55d12f1d 100644
--- a/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v
+++ b/src/SpecificGen/GF41417_32Reflective/CommonBinOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF41417_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v
index b3d00f8c9..92a928bfc 100644
--- a/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v
+++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF41417_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v
index 8a8075739..4c8923dd9 100644
--- a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v
+++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToWire.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF41417_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v
index 19664d936..748e2fd10 100644
--- a/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v
+++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOpFEToZ.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF41417_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v
index 7c23f3be8..d70798964 100644
--- a/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v
+++ b/src/SpecificGen/GF41417_32Reflective/CommonUnOpWireToFE.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF41417_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v
index 4c658f227..fe50d7a26 100644
--- a/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF41417_32Reflective/Reified/AddCoordinates.v
@@ -4,6 +4,7 @@ Require Export Crypto.SpecificGen.GF41417_32.
 Require Export Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Application.
diff --git a/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v
index 1f3516551..db671ccb4 100644
--- a/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v
+++ b/src/SpecificGen/GF41417_32Reflective/Reified/LadderStep.v
@@ -4,6 +4,7 @@ Require Export Crypto.SpecificGen.GF41417_32.
 Require Export Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Application.
diff --git a/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v
index 82f159e25..c08f28dfe 100644
--- a/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v
+++ b/src/SpecificGen/GF41417_32ReflectiveAddCoordinates.v
@@ -9,6 +9,7 @@ Require Export Crypto.SpecificGen.GF41417_32.
 Require Import Crypto.SpecificGen.GF41417_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
diff --git a/src/SpecificGen/GF5211_32Reflective.v b/src/SpecificGen/GF5211_32Reflective.v
index 8c80562de..fe29cae6a 100644
--- a/src/SpecificGen/GF5211_32Reflective.v
+++ b/src/SpecificGen/GF5211_32Reflective.v
@@ -9,6 +9,7 @@ Require Export Crypto.SpecificGen.GF5211_32.
 Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
diff --git a/src/SpecificGen/GF5211_32Reflective/Common.v b/src/SpecificGen/GF5211_32Reflective/Common.v
index 670234315..cd420e99d 100644
--- a/src/SpecificGen/GF5211_32Reflective/Common.v
+++ b/src/SpecificGen/GF5211_32Reflective/Common.v
@@ -4,6 +4,8 @@ Require Export Crypto.SpecificGen.GF5211_32.
 Require Export Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
+Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.
@@ -43,7 +45,7 @@ Definition Expr_n_OpT (count_out : nat) : flat_type base_type
 Fixpoint Expr_nm_OpT (count_in count_out : nat) : type base_type
   := match count_in with
      | 0 => Expr_n_OpT count_out
-     | S n => SmartArrow base_type fe5211_32T (Expr_nm_OpT n count_out)
+     | S n => SmartArrow fe5211_32T (Expr_nm_OpT n count_out)
      end.
 Definition ExprBinOpT : type base_type := Eval compute in Expr_nm_OpT 2 1.
 Definition ExprUnOpT : type base_type := Eval compute in Expr_nm_OpT 1 1.
diff --git a/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v b/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v
index b1da3f12f..da61302b4 100644
--- a/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v
+++ b/src/SpecificGen/GF5211_32Reflective/Common9_4Op.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF5211_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v b/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v
index 2395d7c74..6d4f73920 100644
--- a/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v
+++ b/src/SpecificGen/GF5211_32Reflective/CommonBinOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF5211_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v
index 29652a1e8..d8bc7dcfa 100644
--- a/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v
+++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOp.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF5211_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v
index 9d37b910f..91469dc14 100644
--- a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v
+++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToWire.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF5211_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v
index 9dde1f276..68389da47 100644
--- a/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v
+++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpFEToZ.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF5211_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v b/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v
index e20146853..48b8c853a 100644
--- a/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v
+++ b/src/SpecificGen/GF5211_32Reflective/CommonUnOpWireToFE.v
@@ -2,6 +2,7 @@ Require Export Crypto.SpecificGen.GF5211_32Reflective.Common.
 Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Application.
 Require Import Crypto.Util.Tactics.
 
diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v b/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v
index 85da73838..88b4ab0fd 100644
--- a/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v
+++ b/src/SpecificGen/GF5211_32Reflective/Reified/AddCoordinates.v
@@ -4,6 +4,7 @@ Require Export Crypto.SpecificGen.GF5211_32.
 Require Export Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.Application.
diff --git a/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v
index b05fc64a6..b047b6cd3 100644
--- a/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v
+++ b/src/SpecificGen/GF5211_32Reflective/Reified/LadderStep.v
@@ -4,6 +4,7 @@ Require Export Crypto.SpecificGen.GF5211_32.
 Require Export Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.SmartMap.
 Require Import Crypto.Reflection.Relations.
 Require Import Crypto.Reflection.ExprInversion.
 Require Import Crypto.Reflection.Application.
diff --git a/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v b/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v
index 5284ffbcd..ee7bbb2e2 100644
--- a/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v
+++ b/src/SpecificGen/GF5211_32ReflectiveAddCoordinates.v
@@ -9,6 +9,7 @@ Require Export Crypto.SpecificGen.GF5211_32.
 Require Import Crypto.SpecificGen.GF5211_32BoundedCommon.
 Require Import Crypto.Reflection.Reify.
 Require Import Crypto.Reflection.Syntax.
+Require Import Crypto.Reflection.Map.
 Require Import Crypto.Reflection.Z.Interpretations64.
 Require Crypto.Reflection.Z.Interpretations64.Relations.
 Require Import Crypto.Reflection.Z.Interpretations64.RelationsCombinations.
diff --git a/src/Util/Tactics.v b/src/Util/Tactics.v
index e6f5a1cac..dffd6e581 100644
--- a/src/Util/Tactics.v
+++ b/src/Util/Tactics.v
@@ -4,6 +4,8 @@ Require Export Crypto.Util.Tactics.BreakMatch.
 Require Export Crypto.Util.Tactics.Head.
 Require Export Crypto.Util.Tactics.DestructHyps.
 Require Export Crypto.Util.Tactics.DestructHead.
+Require Export Crypto.Util.Tactics.DoWithHyp.
+Require Export Crypto.Util.Tactics.RewriteHyp.
 Require Export Crypto.Util.Tactics.SpecializeBy.
 Require Export Crypto.Util.Tactics.SplitInContext.
 
@@ -178,53 +180,6 @@ Ltac side_conditions_before_to_side_conditions_after tac_in H :=
     move H after H'; clear H'
   | .. ].
 
-(** Do something with every hypothesis. *)
-Ltac do_with_hyp' tac :=
-  match goal with
-    | [ H : _ |- _ ] => tac H
-  end.
-
-(** Rewrite with any applicable hypothesis. *)
-Tactic Notation "rewrite_hyp" "*" := do_with_hyp' ltac:(fun H => rewrite H).
-Tactic Notation "rewrite_hyp" "->" "*" := do_with_hyp' ltac:(fun H => rewrite -> H).
-Tactic Notation "rewrite_hyp" "<-" "*" := do_with_hyp' ltac:(fun H => rewrite <- H).
-Tactic Notation "rewrite_hyp" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite !H).
-Tactic Notation "rewrite_hyp" "->" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H).
-Tactic Notation "rewrite_hyp" "<-" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H).
-Tactic Notation "rewrite_hyp" "!*" := progress rewrite_hyp ?*.
-Tactic Notation "rewrite_hyp" "->" "!*" := progress rewrite_hyp -> ?*.
-Tactic Notation "rewrite_hyp" "<-" "!*" := progress rewrite_hyp <- ?*.
-
-Tactic Notation "rewrite_hyp" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite H in * ).
-Tactic Notation "rewrite_hyp" "->" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite -> H in * ).
-Tactic Notation "rewrite_hyp" "<-" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite <- H in * ).
-Tactic Notation "rewrite_hyp" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite !H in * ).
-Tactic Notation "rewrite_hyp" "->" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H in * ).
-Tactic Notation "rewrite_hyp" "<-" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H in * ).
-Tactic Notation "rewrite_hyp" "!*" "in" "*" := progress rewrite_hyp ?* in *.
-Tactic Notation "rewrite_hyp" "->" "!*" "in" "*" := progress rewrite_hyp -> ?* in *.
-Tactic Notation "rewrite_hyp" "<-" "!*" "in" "*" := progress rewrite_hyp <- ?* in *.
-
-Tactic Notation "erewrite_hyp" "*" := do_with_hyp' ltac:(fun H => erewrite H).
-Tactic Notation "erewrite_hyp" "->" "*" := do_with_hyp' ltac:(fun H => erewrite -> H).
-Tactic Notation "erewrite_hyp" "<-" "*" := do_with_hyp' ltac:(fun H => erewrite <- H).
-Tactic Notation "erewrite_hyp" "?*" := repeat do_with_hyp' ltac:(fun H => erewrite !H).
-Tactic Notation "erewrite_hyp" "->" "?*" := repeat do_with_hyp' ltac:(fun H => erewrite -> !H).
-Tactic Notation "erewrite_hyp" "<-" "?*" := repeat do_with_hyp' ltac:(fun H => erewrite <- !H).
-Tactic Notation "erewrite_hyp" "!*" := progress erewrite_hyp ?*.
-Tactic Notation "erewrite_hyp" "->" "!*" := progress erewrite_hyp -> ?*.
-Tactic Notation "erewrite_hyp" "<-" "!*" := progress erewrite_hyp <- ?*.
-
-Tactic Notation "erewrite_hyp" "*" "in" "*" := do_with_hyp' ltac:(fun H => erewrite H in * ).
-Tactic Notation "erewrite_hyp" "->" "*" "in" "*" := do_with_hyp' ltac:(fun H => erewrite -> H in * ).
-Tactic Notation "erewrite_hyp" "<-" "*" "in" "*" := do_with_hyp' ltac:(fun H => erewrite <- H in * ).
-Tactic Notation "erewrite_hyp" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => erewrite !H in * ).
-Tactic Notation "erewrite_hyp" "->" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => erewrite -> !H in * ).
-Tactic Notation "erewrite_hyp" "<-" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => erewrite <- !H in * ).
-Tactic Notation "erewrite_hyp" "!*" "in" "*" := progress erewrite_hyp ?* in *.
-Tactic Notation "erewrite_hyp" "->" "!*" "in" "*" := progress erewrite_hyp -> ?* in *.
-Tactic Notation "erewrite_hyp" "<-" "!*" "in" "*" := progress erewrite_hyp <- ?* in *.
-
 (** Execute [progress tac] on all subterms of the goal.  Useful for things like [ring_simplify]. *)
 Ltac tac_on_subterms tac :=
   repeat match goal with
diff --git a/src/Util/Tactics/DoWithHyp.v b/src/Util/Tactics/DoWithHyp.v
new file mode 100644
index 000000000..b31072a63
--- /dev/null
+++ b/src/Util/Tactics/DoWithHyp.v
@@ -0,0 +1,7 @@
+Require Export Crypto.Util.FixCoqMistakes.
+
+(** Do something with every hypothesis. *)
+Ltac do_with_hyp' tac :=
+  match goal with
+    | [ H : _ |- _ ] => tac H
+  end.
diff --git a/src/Util/Tactics/RewriteHyp.v b/src/Util/Tactics/RewriteHyp.v
new file mode 100644
index 000000000..240931e05
--- /dev/null
+++ b/src/Util/Tactics/RewriteHyp.v
@@ -0,0 +1,44 @@
+Require Export Crypto.Util.FixCoqMistakes.
+Require Import Crypto.Util.Tactics.DoWithHyp.
+
+
+(** Rewrite with any applicable hypothesis. *)
+Tactic Notation "rewrite_hyp" "*" := do_with_hyp' ltac:(fun H => rewrite H).
+Tactic Notation "rewrite_hyp" "->" "*" := do_with_hyp' ltac:(fun H => rewrite -> H).
+Tactic Notation "rewrite_hyp" "<-" "*" := do_with_hyp' ltac:(fun H => rewrite <- H).
+Tactic Notation "rewrite_hyp" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite !H).
+Tactic Notation "rewrite_hyp" "->" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H).
+Tactic Notation "rewrite_hyp" "<-" "?*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H).
+Tactic Notation "rewrite_hyp" "!*" := progress rewrite_hyp ?*.
+Tactic Notation "rewrite_hyp" "->" "!*" := progress rewrite_hyp -> ?*.
+Tactic Notation "rewrite_hyp" "<-" "!*" := progress rewrite_hyp <- ?*.
+
+Tactic Notation "rewrite_hyp" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite H in * ).
+Tactic Notation "rewrite_hyp" "->" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite -> H in * ).
+Tactic Notation "rewrite_hyp" "<-" "*" "in" "*" := do_with_hyp' ltac:(fun H => rewrite <- H in * ).
+Tactic Notation "rewrite_hyp" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite !H in * ).
+Tactic Notation "rewrite_hyp" "->" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite -> !H in * ).
+Tactic Notation "rewrite_hyp" "<-" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => rewrite <- !H in * ).
+Tactic Notation "rewrite_hyp" "!*" "in" "*" := progress rewrite_hyp ?* in *.
+Tactic Notation "rewrite_hyp" "->" "!*" "in" "*" := progress rewrite_hyp -> ?* in *.
+Tactic Notation "rewrite_hyp" "<-" "!*" "in" "*" := progress rewrite_hyp <- ?* in *.
+
+Tactic Notation "erewrite_hyp" "*" := do_with_hyp' ltac:(fun H => erewrite H).
+Tactic Notation "erewrite_hyp" "->" "*" := do_with_hyp' ltac:(fun H => erewrite -> H).
+Tactic Notation "erewrite_hyp" "<-" "*" := do_with_hyp' ltac:(fun H => erewrite <- H).
+Tactic Notation "erewrite_hyp" "?*" := repeat do_with_hyp' ltac:(fun H => erewrite !H).
+Tactic Notation "erewrite_hyp" "->" "?*" := repeat do_with_hyp' ltac:(fun H => erewrite -> !H).
+Tactic Notation "erewrite_hyp" "<-" "?*" := repeat do_with_hyp' ltac:(fun H => erewrite <- !H).
+Tactic Notation "erewrite_hyp" "!*" := progress erewrite_hyp ?*.
+Tactic Notation "erewrite_hyp" "->" "!*" := progress erewrite_hyp -> ?*.
+Tactic Notation "erewrite_hyp" "<-" "!*" := progress erewrite_hyp <- ?*.
+
+Tactic Notation "erewrite_hyp" "*" "in" "*" := do_with_hyp' ltac:(fun H => erewrite H in * ).
+Tactic Notation "erewrite_hyp" "->" "*" "in" "*" := do_with_hyp' ltac:(fun H => erewrite -> H in * ).
+Tactic Notation "erewrite_hyp" "<-" "*" "in" "*" := do_with_hyp' ltac:(fun H => erewrite <- H in * ).
+Tactic Notation "erewrite_hyp" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => erewrite !H in * ).
+Tactic Notation "erewrite_hyp" "->" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => erewrite -> !H in * ).
+Tactic Notation "erewrite_hyp" "<-" "?*" "in" "*" := repeat do_with_hyp' ltac:(fun H => erewrite <- !H in * ).
+Tactic Notation "erewrite_hyp" "!*" "in" "*" := progress erewrite_hyp ?* in *.
+Tactic Notation "erewrite_hyp" "->" "!*" "in" "*" := progress erewrite_hyp -> ?* in *.
+Tactic Notation "erewrite_hyp" "<-" "!*" "in" "*" := progress erewrite_hyp <- ?* in *.