Switch to a more precise version of interp_related for rewrites

This version is hopefully the right one.  It seems to be basically
exactly what we want to say, and no more and no less.  The rule for
let-ins, which is almost the only freedom we have here, is chosen to
match exactly with the rule for App+Abs.  Note that using Leibniz
equality is essential in the places where it's used.  The recursive
relation here might actually be a bit clearer as an inductive relation,
but I wanted it to simplify under reduction.

After     | File Name                                                            | Before    || Change    | % Change
--------------------------------------------------------------------------------------------------------------------
30m04.79s | Total                                                                | 29m51.25s || +0m13.54s | +0.75%
--------------------------------------------------------------------------------------------------------------------
1m53.11s  | Experiments/NewPipeline/RewriterRulesInterpGood.vo                   | 1m35.74s  || +0m17.36s | +18.14%
0m19.40s  | Experiments/NewPipeline/RewriterWf1.vo                               | 0m24.54s  || -0m05.14s | -20.94%
6m13.78s  | Experiments/NewPipeline/SlowPrimeSynthesisExamples.vo                | 6m14.86s  || -0m01.08s | -0.28%
4m39.23s  | Experiments/NewPipeline/Toplevel1.vo                                 | 4m38.21s  || +0m01.02s | +0.36%
1m31.62s  | Experiments/NewPipeline/Toplevel2.vo                                 | 1m32.68s  || -0m01.06s | -1.14%
0m40.01s  | Experiments/NewPipeline/AbstractInterpretationWf.vo                  | 0m38.77s  || +0m01.23s | +3.19%
3m19.74s  | p384_32.c                                                            | 3m19.71s  || +0m00.03s | +0.01%
1m58.86s  | Experiments/NewPipeline/RewriterWf2.vo                               | 1m58.30s  || +0m00.56s | +0.47%
1m02.04s  | Experiments/NewPipeline/RewriterRulesGood.vo                         | 1m02.41s  || -0m00.36s | -0.59%
0m40.71s  | p521_32.c                                                            | 0m40.51s  || +0m00.20s | +0.49%
0m39.90s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery    | 0m39.85s  || +0m00.04s | +0.12%
0m36.76s  | Experiments/NewPipeline/Rewriter.vo                                  | 0m36.81s  || -0m00.05s | -0.13%
0m35.34s  | Experiments/NewPipeline/LanguageInversion.vo                         | 0m35.16s  || +0m00.18s | +0.51%
0m33.80s  | p521_64.c                                                            | 0m33.82s  || -0m00.02s | -0.05%
0m28.97s  | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypesProofs.vo    | 0m29.54s  || -0m00.57s | -1.92%
0m27.65s  | Experiments/NewPipeline/LanguageWf.vo                                | 0m28.11s  || -0m00.46s | -1.63%
0m25.94s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas        | 0m25.39s  || +0m00.55s | +2.16%
0m25.63s  | Experiments/NewPipeline/UnderLetsProofs.vo                           | 0m25.15s  || +0m00.48s | +1.90%
0m22.84s  | Experiments/NewPipeline/AbstractInterpretationZRangeProofs.vo        | 0m23.11s  || -0m00.26s | -1.16%
0m18.51s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas          | 0m18.69s  || -0m00.17s | -0.96%
0m17.42s  | Experiments/NewPipeline/AbstractInterpretationProofs.vo              | 0m17.29s  || +0m00.13s | +0.75%
0m15.12s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery      | 0m14.96s  || +0m00.15s | +1.06%
0m14.43s  | secp256k1_32.c                                                       | 0m14.22s  || +0m00.20s | +1.47%
0m14.19s  | p256_32.c                                                            | 0m14.46s  || -0m00.27s | -1.86%
0m12.72s  | Experiments/NewPipeline/CStringification.vo                          | 0m12.80s  || -0m00.08s | -0.62%
0m10.88s  | p384_64.c                                                            | 0m10.99s  || -0m00.10s | -1.00%
0m09.16s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas          | 0m08.87s  || +0m00.29s | +3.26%
0m09.14s  | Experiments/NewPipeline/ExtractionOCaml/word_by_word_montgomery.ml   | 0m09.33s  || -0m00.18s | -2.03%
0m07.96s  | Experiments/NewPipeline/GENERATEDIdentifiersWithoutTypes.vo          | 0m07.96s  || +0m00.00s | +0.00%
0m06.61s  | p224_32.c                                                            | 0m06.52s  || +0m00.09s | +1.38%
0m06.37s  | Experiments/NewPipeline/ExtractionOCaml/unsaturated_solinas.ml       | 0m06.29s  || +0m00.08s | +1.27%
0m05.96s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas            | 0m05.60s  || +0m00.36s | +6.42%
0m05.92s  | Experiments/NewPipeline/ExtractionHaskell/word_by_word_montgomery.hs | 0m05.82s  || +0m00.09s | +1.71%
0m04.70s  | Experiments/NewPipeline/ExtractionHaskell/unsaturated_solinas.hs     | 0m04.35s  || +0m00.35s | +8.04%
0m04.50s  | Experiments/NewPipeline/ExtractionOCaml/saturated_solinas.ml         | 0m04.63s  || -0m00.12s | -2.80%
0m03.82s  | Experiments/NewPipeline/ExtractionHaskell/saturated_solinas.hs       | 0m03.62s  || +0m00.19s | +5.52%
0m02.62s  | Experiments/NewPipeline/MiscCompilerPassesProofs.vo                  | 0m02.56s  || +0m00.06s | +2.34%
0m02.31s  | curve25519_32.c                                                      | 0m02.40s  || -0m00.08s | -3.74%
0m02.09s  | secp256k1_64.c                                                       | 0m02.18s  || -0m00.09s | -4.12%
0m02.05s  | p224_64.c                                                            | 0m02.04s  || +0m00.00s | +0.49%
0m01.96s  | p256_64.c                                                            | 0m01.94s  || +0m00.02s | +1.03%
0m01.56s  | curve25519_64.c                                                      | 0m01.54s  || +0m00.02s | +1.29%
0m01.53s  | Experiments/NewPipeline/CLI.vo                                       | 0m01.57s  || -0m00.04s | -2.54%
0m01.26s  | Experiments/NewPipeline/StandaloneHaskellMain.vo                     | 0m01.26s  || +0m00.00s | +0.00%
0m01.22s  | Experiments/NewPipeline/Language.vo                                  | 0m01.26s  || -0m00.04s | -3.17%
0m01.22s  | Experiments/NewPipeline/StandaloneOCamlMain.vo                       | 0m01.21s  || +0m00.01s | +0.82%
0m01.08s  | Experiments/NewPipeline/CompilersTestCases.vo                        | 0m00.99s  || +0m00.09s | +9.09%
0m01.06s  | Experiments/NewPipeline/AbstractInterpretation.vo                    | 0m01.02s  || +0m00.04s | +3.92%
0m00.87s  | Experiments/NewPipeline/RewriterProofs.vo                            | 0m00.97s  || -0m00.09s | -10.30%
0m00.74s  | Experiments/NewPipeline/MiscCompilerPasses.vo                        | 0m00.72s  || +0m00.02s | +2.77%
0m00.48s  | Experiments/NewPipeline/UnderLets.vo                                 | 0m00.52s  || -0m00.04s | -7.69%

8 files changed, 746 insertions, 618 deletions

diff --git a/src/Experiments/NewPipeline/Language.v b/src/Experiments/NewPipeline/Language.v
index cc8dcff86..c129675c9 100644
--- a/src/Experiments/NewPipeline/Language.v
+++ b/src/Experiments/NewPipeline/Language.v
@@ -452,6 +452,39 @@ Module Compilers.
                @interp _ _ _ interp_ident _ (f y)
          end.
 
+    Section with_interp.
+      Context {base_type : Type}
+              {ident : type base_type -> Type}
+              {interp_base_type : base_type -> Type}
+              (interp_ident : forall t, ident t -> type.interp interp_base_type t).
+
+      Fixpoint interp_related {t} (e : @expr base_type ident (type.interp interp_base_type) t) : type.interp interp_base_type t -> Prop
+        := match e in expr t return type.interp interp_base_type t -> Prop with
+           | expr.Var t v1 => fun v2 => v1 == v2
+           | expr.App s d f x
+             => fun v2
+                => exists fv xv,
+                    @interp_related _ f fv
+                    /\ @interp_related _ x xv
+                    /\ fv xv = v2
+           | expr.Ident t idc
+             => fun v2 => interp_ident _ idc == v2
+           | expr.Abs s d f1
+             => fun f2
+                => forall x1 x2,
+                    x1 == x2
+                    -> @interp_related d (f1 x1) (f2 x2)
+           | expr.LetIn s d x f (* combine the App rule with the Abs rule *)
+             => fun v2
+                => exists fv xv,
+                    @interp_related _ x xv
+                    /\ (forall x1 x2,
+                           x1 == x2
+                           -> @interp_related d (f x1) (fv x2))
+                    /\ fv xv = v2
+           end.
+    End with_interp.
+
     Definition Expr {base_type ident} t := forall var, @expr base_type ident var t.
     Definition APP {base_type ident s d} (f : Expr (s -> d)) (x : Expr s) : Expr d
       := fun var => @App base_type ident var s d (f var) (x var).
diff --git a/src/Experiments/NewPipeline/LanguageInversion.v b/src/Experiments/NewPipeline/LanguageInversion.v
index eb67f5355..f5cc89b4f 100644
--- a/src/Experiments/NewPipeline/LanguageInversion.v
+++ b/src/Experiments/NewPipeline/LanguageInversion.v
@@ -599,6 +599,51 @@ Module Compilers.
       Proof. split; intro; subst; apply reflect_reify_list || apply reflect_list_Some; assumption. Qed.
     End with_var2.
 
+    Section with_interp.
+      Context {cast_outside_of_range : ZRange.zrange -> BinInt.Z -> BinInt.Z}.
+      Local Notation ident_interp := (@ident.gen_interp cast_outside_of_range).
+
+      Lemma reify_list_interp_related_iff {t ls v}
+        : expr.interp_related (@ident_interp) (reify_list (t:=t) ls) v
+          <-> List.Forall2 (expr.interp_related (@ident_interp)) ls v.
+      Proof using Type.
+        revert v; induction ls as [|l ls IHls], v as [|v vs].
+        all: repeat first [ rewrite expr.reify_list_nil
+                          | rewrite expr.reify_list_cons
+                          | progress cbn [expr.interp_related ident.gen_interp type.related] in *
+                          | progress cbv [Morphisms.respectful] in *
+                          | progress destruct_head'_ex
+                          | progress destruct_head'_and
+                          | progress subst
+                          | reflexivity
+                          | assumption
+                          | apply conj
+                          | progress intros
+                          | match goal with
+                            | [ H : List.Forall2 _ nil _ |- _ ] => inversion_clear H
+                            | [ H : List.Forall2 _ (cons _ _) _ |- _ ] => inversion_clear H
+                            | [ |- List.Forall2 _ _ _ ] => constructor
+                            | [ H : nil = cons _ _ |- _ ] => solve [ inversion H ]
+                            | [ H : cons _ _ = nil |- _ ] => solve [ inversion H ]
+                            | [ H : cons _ _ = cons _ _ |- _ ] => inversion H; clear H
+                            | [ H : forall x y, x = y -> _ |- _ ] => specialize (fun x => H x x eq_refl)
+                            | [ H : forall a x y, x = y -> _ |- _ ] => specialize (fun a x => H a x x eq_refl)
+                            | [ H : forall x y, _ = ?f x y, H' : context[?f _ _] |- _ ] => rewrite <- H in H'
+                            | [ H : _ |- _ ] => apply H; clear H
+                            | [ |- ex _ ] => eexists
+                            end ].
+      Qed.
+
+      Lemma reflect_list_interp_related_iff {t ls ls' v}
+            (Hls : invert_expr.reflect_list (t:=t) ls = Some ls')
+        : List.Forall2 (expr.interp_related (@ident_interp)) ls' v
+          <-> expr.interp_related (@ident_interp) ls v.
+      Proof using Type.
+        apply reflect_list_Some in Hls; subst.
+        rewrite reify_list_interp_related_iff; reflexivity.
+      Qed.
+    End with_interp.
+
     Ltac invert_subst_step_helper guard_tac :=
       cbv [defaults.type_base] in *;
       match goal with
diff --git a/src/Experiments/NewPipeline/LanguageWf.v b/src/Experiments/NewPipeline/LanguageWf.v
index 4ed42814d..ccfaa0365 100644
--- a/src/Experiments/NewPipeline/LanguageWf.v
+++ b/src/Experiments/NewPipeline/LanguageWf.v
@@ -565,6 +565,25 @@ Hint Extern 10 (Proper ?R ?x) => simple eapply (@PER_valid_r _ R); [ | | solve [
         End inversion.
       End with_var.
 
+      Section with_interp.
+        Context {interp_base_type : base_type -> Type}
+                {interp_ident : forall t, ident t -> type.interp interp_base_type t}.
+
+        Lemma eqv_of_interp_related {t e v}
+          : expr.interp_related interp_ident e v
+            -> @type.eqv t (expr.interp interp_ident e) v.
+        Proof using Type.
+          induction e; cbn [expr.interp_related expr.interp type.related]; cbv [respectful LetIn.Let_In].
+          all: repeat first [ progress intros
+                            | assumption
+                            | solve [ eauto ]
+                            | progress destruct_head'_ex
+                            | progress destruct_head'_and
+                            | progress subst
+                            | match goal with H : _ |- _ => apply H; clear H end ].
+        Qed.
+      End with_interp.
+
       Section with_var3.
         Context {var1 var2 var3 : type.type base_type -> Type}.
         Local Notation wfvP := (fun t => (var1 t * var2 t * var3 t)%type).
diff --git a/src/Experiments/NewPipeline/Rewriter.v b/src/Experiments/NewPipeline/Rewriter.v
index af2d2617b..d4746687e 100644
--- a/src/Experiments/NewPipeline/Rewriter.v
+++ b/src/Experiments/NewPipeline/Rewriter.v
@@ -637,86 +637,86 @@ Module Compilers.
           := reveal_rawexpr_cps_gen None e.
 
         (** First, the uncurried form *)
-        Fixpoint unification_resultT' {t} (p : pattern t) (evm : EvarMap) : Type
+        Fixpoint unification_resultT' {var} {t} (p : pattern t) (evm : EvarMap) : Type
           := match p return Type with
-             | pattern.Wildcard t => value (pattern.type.subst_default t evm)
+             | pattern.Wildcard t => var (pattern.type.subst_default t evm)
              | pattern.Ident t idc => type_of_list (pident_arg_types t idc)
              | pattern.App s d f x
-               => @unification_resultT' _ f evm * @unification_resultT' _ x evm
+               => @unification_resultT' var _ f evm * @unification_resultT' var _ x evm
              end%type.
 
-        Fixpoint with_unification_resultT' {t} (p : pattern t) (evm : EvarMap) (K : Type) : Type
+        Fixpoint with_unification_resultT' {var} {t} (p : pattern t) (evm : EvarMap) (K : Type) : Type
           := match p return Type with
-             | pattern.Wildcard t => value (pattern.type.subst_default t evm) -> K
+             | pattern.Wildcard t => var (pattern.type.subst_default t evm) -> K
              | pattern.Ident t idc => type_of_list_cps K (pident_arg_types t idc)
              | pattern.App s d f x
-               => @with_unification_resultT' _ f evm (@with_unification_resultT' _ x evm K)
+               => @with_unification_resultT' var _ f evm (@with_unification_resultT' var _ x evm K)
              end%type.
 
-        Fixpoint app_with_unification_resultT' {t p evm K} {struct p}
-          : @with_unification_resultT' t p evm K -> @unification_resultT' t p evm -> K
+        Fixpoint app_with_unification_resultT' {var t p evm K} {struct p}
+          : @with_unification_resultT' var t p evm K -> @unification_resultT' var t p evm -> K
           := match p return with_unification_resultT' p evm K -> unification_resultT' p evm -> K with
              | pattern.Wildcard t => fun f x => f x
              | pattern.Ident t idc => app_type_of_list
              | pattern.App s d f x
                => fun F (xy : unification_resultT' f _ * unification_resultT' x _)
                   => @app_with_unification_resultT'
-                       _ x _ _
+                       _ _ x _ _
                        (@app_with_unification_resultT'
-                          _ f _ _ F (fst xy))
+                          _ _ f _ _ F (fst xy))
                        (snd xy)
              end.
 
         (** TODO: Maybe have a fancier version of this that doesn't
              actually need to insert casts, by doing a fixpoint on the
              list of elements / the evar map *)
-        Fixpoint app_transport_with_unification_resultT'_cps {t p evm1 evm2 K} {struct p}
-          : @with_unification_resultT' t p evm1 K -> @unification_resultT' t p evm2 -> forall T, (K -> option T) -> option T
+        Fixpoint app_transport_with_unification_resultT'_cps {var t p evm1 evm2 K} {struct p}
+          : @with_unification_resultT' var t p evm1 K -> @unification_resultT' var t p evm2 -> forall T, (K -> option T) -> option T
           := fun f x T k
              => match p return with_unification_resultT' p evm1 K -> unification_resultT' p evm2 -> option T with
                 | pattern.Wildcard t
                   => fun f x
-                     => (tr <- type.try_make_transport_cps base.try_make_transport_cps value _ _;
+                     => (tr <- type.try_make_transport_cps base.try_make_transport_cps var _ _;
                            (tr <- tr;
                               k (f (tr x)))%option)%cps
              | pattern.Ident t idc => fun f x => k (app_type_of_list f x)
              | pattern.App s d f x
                => fun F (xy : unification_resultT' f _ * unification_resultT' x _)
                   => @app_transport_with_unification_resultT'_cps
-                       _ f _ _ _ F (fst xy) T
+                       _ _ f _ _ _ F (fst xy) T
                        (fun F'
                         => @app_transport_with_unification_resultT'_cps
-                             _ x _ _ _ F' (snd xy) T
+                             _ _ x _ _ _ F' (snd xy) T
                              (fun x' => k x'))
              end%option f x.
 
-        Fixpoint under_with_unification_resultT' {t p evm K1 K2}
+        Fixpoint under_with_unification_resultT' {var t p evm K1 K2}
                  (F : K1 -> K2)
                  {struct p}
-          : @with_unification_resultT' t p evm K1 -> @with_unification_resultT' t p evm K2
+          : @with_unification_resultT' var t p evm K1 -> @with_unification_resultT' var t p evm K2
           := match p return with_unification_resultT' p evm K1 -> with_unification_resultT' p evm K2 with
              | pattern.Wildcard t => fun f v => F (f v)
              | pattern.Ident t idc => under_type_of_list_cps F
              | pattern.App s d f x
                => @under_with_unification_resultT'
-                    _ f evm _ _
-                    (@under_with_unification_resultT' _ x evm _ _ F)
+                    _ _ f evm _ _
+                    (@under_with_unification_resultT' _ _ x evm _ _ F)
              end.
 
         Definition ident_collect_vars := (fun t idc => fold_right PositiveSet.union PositiveSet.empty (List.map pattern.type.collect_vars (type_vars_of_pident t idc))).
 
-        Definition with_unification_resultT {t} (p : pattern t) (K : type -> Type) : Type
+        Definition with_unification_resultT {var t} (p : pattern t) (K : type -> Type) : Type
           := pattern.type.forall_vars
                (@pattern.collect_vars
                   _ ident_collect_vars
                   t p)
-               (fun evm => with_unification_resultT' p evm (K (pattern.type.subst_default t evm))).
+               (fun evm => @with_unification_resultT' var t p evm (K (pattern.type.subst_default t evm))).
 
-        Definition unification_resultT {t} (p : pattern t) : Type
-          := { evm : EvarMap & unification_resultT' p evm }.
+        Definition unification_resultT {var t} (p : pattern t) : Type
+          := { evm : EvarMap & @unification_resultT' var t p evm }.
 
-        Definition app_with_unification_resultT_cps {t p K}
-          : @with_unification_resultT t p K -> @unification_resultT t p -> forall T, ({ evm' : _ & K (pattern.type.subst_default t evm') } -> option T) -> option T
+        Definition app_with_unification_resultT_cps {var t p K}
+          : @with_unification_resultT var t p K -> @unification_resultT var t p -> forall T, ({ evm' : _ & K (pattern.type.subst_default t evm') } -> option T) -> option T
           := fun f x T k
              => (f' <- pattern.type.app_forall_vars f (projT1 x);
                    app_transport_with_unification_resultT'_cps
@@ -724,9 +724,9 @@ Module Compilers.
                      (fun fx
                       => k (existT _ _ fx)))%option.
 
-        Definition under_with_unification_resultT {t p K1 K2}
+        Definition under_with_unification_resultT {var t p K1 K2}
                  (F : forall evm, K1 (pattern.type.subst_default t evm) -> K2 (pattern.type.subst_default t evm))
-          : @with_unification_resultT t p K1 -> @with_unification_resultT t p K2
+          : @with_unification_resultT var t p K1 -> @with_unification_resultT var t p K2
           := pattern.type.under_forall_vars
                (fun evm => under_with_unification_resultT' (F evm)).
 
@@ -960,14 +960,14 @@ Module Compilers.
              | false, false => fun x => Some (UnderLets.Base x)
              end%cps.
 
-        Definition with_unif_rewrite_ruleTP_gen {t} (p : pattern t) (should_do_again : bool) (with_opt : bool) (under_lets : bool)
-          := with_unification_resultT p (fun t => deep_rewrite_ruleTP_gen' should_do_again with_opt under_lets t).
+        Definition with_unif_rewrite_ruleTP_gen {var t} (p : pattern t) (should_do_again : bool) (with_opt : bool) (under_lets : bool)
+          := @with_unification_resultT var t p (fun t => deep_rewrite_ruleTP_gen' should_do_again with_opt under_lets t).
 
         Record rewrite_rule_data {t} {p : pattern t} :=
           { rew_should_do_again : bool;
             rew_with_opt : bool;
             rew_under_lets : bool;
-            rew_replacement : with_unif_rewrite_ruleTP_gen p rew_should_do_again rew_with_opt rew_under_lets }.
+            rew_replacement : @with_unif_rewrite_ruleTP_gen value t p rew_should_do_again rew_with_opt rew_under_lets }.
 
         Definition rewrite_ruleTP
           := (fun p : anypattern => @rewrite_rule_data _ (pattern.pattern_of_anypattern p)).
@@ -1250,10 +1250,10 @@ Module Compilers.
         Coercion ptype_base : pattern.base.type >-> ptype.
         Local Notation ident_collect_vars := (@ident_collect_vars pattern.ident (@pattern.ident.type_vars)).
         Local Notation collect_vars := (@pattern.collect_vars pattern.ident (@ident_collect_vars)).
-        Local Notation with_unification_resultT' := (@with_unification_resultT' ident var pattern.ident (@pattern.ident.arg_types)).
-        Local Notation with_unification_resultT := (@with_unification_resultT ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)).
-        Local Notation under_with_unification_resultT' := (@under_with_unification_resultT' ident var pattern.ident (@pattern.ident.arg_types)).
-        Local Notation under_with_unification_resultT := (@under_with_unification_resultT ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)).
+        Local Notation with_unification_resultT' := (@with_unification_resultT' pattern.ident (@pattern.ident.arg_types) value).
+        Local Notation with_unification_resultT := (@with_unification_resultT pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) value).
+        Local Notation under_with_unification_resultT' := (@under_with_unification_resultT' pattern.ident (@pattern.ident.arg_types) value).
+        Local Notation under_with_unification_resultT := (@under_with_unification_resultT pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars) value).
         Local Notation rewrite_ruleTP := (@rewrite_ruleTP ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)).
         Local Notation rewrite_ruleT := (@rewrite_ruleT ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)).
         Local Notation rewrite_rule_data := (@rewrite_rule_data ident var pattern.ident (@pattern.ident.arg_types) (@pattern.ident.type_vars)).
diff --git a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
index bb62228b6..684c027a1 100644
--- a/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
+++ b/src/Experiments/NewPipeline/RewriterRulesInterpGood.v
@@ -33,9 +33,12 @@ Require Import Crypto.Util.Tactics.SpecializeAllWays.
 Require Import Crypto.Util.Tactics.SpecializeBy.
 Require Import Crypto.Util.Tactics.RewriteHyp.
 Require Import Crypto.Util.Tactics.Head.
+Require Import Crypto.Util.Tactics.SetEvars.
+Require Import Crypto.Util.Tactics.SubstEvars.
 Require Import Crypto.Util.Prod.
 Require Import Crypto.Util.Bool.
 Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.ListUtil.Forall.
 Require Import Crypto.Util.ListUtil.ForallIn.
 Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Option.
@@ -101,7 +104,7 @@ Module Compilers.
       Local Ltac do_cbv0 :=
         cbv [id
                Compile.rewrite_rules_interp_goodT_curried
-               Compile.rewrite_rule_data_interp_goodT_curried Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps Compile.under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT Compile.pattern_default_interp pattern.type.under_forall_vars_relation pattern.type.under_forall_vars_relation1 Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.under_type_of_list_relation_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related Compile.value'_interp_related].
+               Compile.rewrite_rule_data_interp_goodT_curried Compile.under_with_unification_resultT_relation_hetero Compile.under_with_unification_resultT'_relation_hetero Compile.wf_with_unification_resultT Compile.under_type_of_list_relation_cps Compile.under_type_of_list_relation1_cps pattern.pattern_of_anypattern pattern.type_of_anypattern Compile.rew_replacement Compile.rew_should_do_again Compile.rew_with_opt Compile.rew_under_lets Compile.wf_with_unification_resultT Compile.pattern_default_interp pattern.type.under_forall_vars_relation pattern.type.under_forall_vars_relation1 Compile.deep_rewrite_ruleTP_gen Compile.with_unification_resultT' pattern.ident.arg_types pattern.type.lam_forall_vars Compile.pattern_default_interp' pattern.collect_vars PositiveMap.empty Compile.ident_collect_vars pattern.ident.type_vars pattern.type.collect_vars PositiveSet.elements PositiveSet.union pattern.base.collect_vars PositiveSet.empty PositiveSet.xelements Compile.lam_type_of_list id pattern.ident.to_typed Compile.under_type_of_list_relation_cps Compile.deep_rewrite_ruleTP_gen_good_relation Compile.normalize_deep_rewrite_rule pattern.type.subst_default PositiveSet.add PositiveSet.rev PositiveSet.rev_append PositiveMap.add Compile.option_bind' Compile.wf_value Compile.value pattern.base.subst_default PositiveMap.find Compile.rewrite_ruleTP ident.smart_Literal Compile.value_interp_related].
       Local Ltac do_cbv :=
         do_cbv0;
         cbv [List.map List.fold_right List.rev list_rect orb List.app].
@@ -125,16 +128,59 @@ Module Compilers.
                        | [ |- _ /\ _ ] => split; [ intros; exact I | ]
                        end
                      | progress cbn [eq_rect] in * ];
-        cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.gen_interp] in *.
+        cbn [fst snd base.interp base.base_interp type.interp projT1 projT2 UnderLets.interp expr.interp type.related ident.gen_interp UnderLets.interp_related] in *.
+
+      Ltac recurse_interp_related_step :=
+        let do_replace v :=
+            ((tryif is_evar v then fail else idtac);
+             let v' := open_constr:(_) in
+             let v'' := fresh in
+             cut (v = v'); [ generalize v; intros v'' ?; subst v'' | symmetry ]) in
+        match goal with
+        | _ => progress cbn [Compile.reify_expr]
+        | [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand
+        | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand
+        | [ |- expr.interp_related ?ident_interp ?f ?v ]
+          => do_replace v
+        | [ |- exists (fv : ?T1 -> ?T2) (ev : ?T1),
+              _ /\ _ /\ fv ev = ?x ]
+          => lazymatch T1 with Z => idtac | (Z * Z)%type => idtac end;
+             lazymatch T2 with Z => idtac | (Z * Z)%type => idtac end;
+             first [ do_replace x
+                   | is_evar x; do 2 eexists; repeat apply conj; [ | | reflexivity ] ]
+        | _ => progress intros
+        | [ |- expr.interp_related _ _ ?ev ] => is_evar ev; eassumption
+        | [ |- expr.interp_related _ (?f @ ?x) ?ev ]
+          => is_evar ev;
+             let fh := fresh in
+             let xh := fresh in
+             set (fh := f); set (xh := x); cbn [expr.interp_related]; subst fh xh;
+             do 2 eexists; repeat apply conj; [ | | reflexivity ]
+        | [ |- expr.interp_related _ (expr.Abs ?f) _ ]
+          => let fh := fresh in set (fh := f); cbn [expr.interp_related]; subst fh
+        | [ |- expr.interp_related _ (expr.Ident ?idc) ?ev ]
+          => is_evar ev;
+             cbn [expr.interp_related]; apply ident.gen_interp_Proper; reflexivity
+        | [ |- _ = _ :> ?T ]
+          => lazymatch T with
+             | BinInt.Z => idtac
+             | (BinInt.Z * BinInt.Z)%type => idtac
+             end;
+             progress cbn [ident_interp fst snd]
+        | [ |- ?x = ?y ] => tryif first [ has_evar x | has_evar y ] then fail else (progress subst)
+        | [ |- ?x = ?x ] => tryif has_evar x then fail else reflexivity
+        | [ |- ?ev = _ ] => is_evar ev; reflexivity
+        | [ |- _ = ?ev ] => is_evar ev; reflexivity
+        end.
 
       Local Ltac interp_good_t_step :=
         first [ reflexivity
               | match goal with
-                | [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand
-                | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand
+                (*| [ |- context[(fst ?x, snd ?x)] ] => progress eta_expand
+                | [ |- context[match ?x with pair a b => _ end] ] => progress eta_expand*)
                 | [ H : ?x = true, H' : ?x = false |- _ ] => exfalso; clear -H H'; congruence
                 end
-              | progress cbn [expr.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr] in *
+              | progress cbn [expr.interp ident.gen_interp fst snd Compile.reify Compile.reflect Compile.wf_value' Compile.value' Option.bind UnderLets.interp list_case type.interp base.interp base.base_interp ident.to_fancy invert_Some ident.fancy.interp ident.fancy.interp_with_wordmax Compile.reify_expr bool_rect UnderLets.interp_related type.related] in *
               | progress cbv [Compile.option_bind' respectful] in *
               | progress fold (@type.interp _ base.interp)
               | progress fold (@base.interp)
@@ -155,16 +201,117 @@ Module Compilers.
                 | [ |- context[UnderLets.interp _ (list_rect _ _ _ _)] ] => rewrite UnderLets_interp_list_rect
                 | [ |- context[UnderLets.interp _ (UnderLets.splice _ _)] ] => rewrite UnderLets.interp_splice
                 | [ |- context[list_rect _ _ _ (List.map _ _)] ] => rewrite list_rect_map
-                | [ |- list_rect _ _ _ _ = List.app ?ls1 ?ls2 ]
+                | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (List.app ?ls1 ?ls2) ]
                   =>  rewrite (eq_app_list_rect ls1 ls2)
-                | [ |- list_rect _ _ _ _ = @flat_map ?A ?B ?f ?ls ]
+                | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@flat_map ?A ?B ?f ?ls) ]
                   =>  rewrite (@eq_flat_map_list_rect A B f ls)
-                | [ |- list_rect _ _ _ _ = @partition ?A ?f ?ls ]
+                | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@partition ?A ?f ?ls) ]
                   =>  rewrite (@eq_partition_list_rect A f ls)
-                | [ |- list_rect _ _ _ _ = @List.map ?A ?B ?f ?ls ]
+                | [ |- UnderLets.interp_related _ _ (list_rect _ _ _ _) (@List.map ?A ?B ?f ?ls) ]
                   => rewrite (@eq_map_list_rect A B f ls)
-                | [ |- _ = @fold_right ?A ?B ?f ?v ?ls ]
+                | [ |- UnderLets.interp_related _ _ _ (@fold_right ?A ?B ?f ?v ?ls) ]
                   =>  rewrite (@eq_fold_right_list_rect A B f v ls)
+                | [ |- context[expr.interp_related _ (reify_list _)] ]
+                  => rewrite expr.reify_list_interp_related_iff
+                | [ H : context[expr.interp_related _ (reify_list _)] |- _ ]
+                  => rewrite expr.reify_list_interp_related_iff in H
+                | [ |- context[Forall2 _ (List.map _ _) _] ] => rewrite Forall2_map_l_iff
+                | [ |- context[Forall2 _ _ (List.map _ _)] ] => rewrite Forall2_map_r_iff
+                | [ |- context[Forall2 _ (List.repeat _ _) (List.repeat _ _)] ] => rewrite Forall2_repeat_iff
+                | [ |- context[Forall2 _ (List.rev _) (List.rev _)] ] => rewrite Forall2_rev_iff
+                | [ |- context[Forall2 _ ?x ?x] ] => rewrite Forall2_Forall; cbv [Proper]
+                | [ |- context[Forall _ (seq _ _)] ] => rewrite Forall_seq
+                | [ H : Forall2 ?R ?l1 ?l2 |- Forall2 ?R (List.firstn ?n ?l1) (List.firstn ?n ?l2) ]
+                  => apply Forall2_firstn, H
+                | [ H : Forall2 ?R ?l1 ?l2 |- Forall2 ?R (List.skipn ?n ?l1) (List.skipn ?n ?l2) ]
+                  => apply Forall2_skipn, H
+                | [ |- Forall2 ?R (List.combine _ _) (List.combine _ _) ]
+                  => eapply Forall2_combine; [ | eassumption | eassumption ]
+                | [ H : List.Forall2 _ ?l1 ?l2, H' : ?R ?v1 ?v2 |- ?R (nth_default ?v1 ?l1 ?x) (nth_default ?v2 ?l2 ?x) ]
+                  => apply Forall2_forall_iff''; split; assumption
+                | [ H : List.Forall2 _ ?x ?y |- List.length ?x = List.length ?y ]
+                  => eapply eq_length_Forall2, H
+                | [ |- exists fv xv, _ /\ _ /\ fv xv = ?f ?x ]
+                  => exists f, x; repeat apply conj; [ solve [ repeat interp_good_t_step ] | | reflexivity ]
+                | [ |- _ /\ ?x = ?x ] => split; [ | reflexivity ]
+                | [ |- UnderLets.interp_related
+                         ?ident_interp ?R
+                         (list_rect
+                            (fun _ : list (expr ?A) => UnderLets.UnderLets _ _ _ ?B)
+                            ?Pnil
+                            ?Pcons
+                            ?ls)
+                         (list_rect
+                            (fun _ : list _ => ?B')
+                            ?Pnil'
+                            ?Pcons'
+                            ?ls') ]
+                  => apply (@UnderLets.list_rect_interp_related _ _ _ ident_interp A B Pnil Pcons ls B' Pnil' Pcons' ls' R)
+                | [ |- UnderLets.interp_related _ _ (nat_rect _ _ _ _) (nat_rect _ _ _ _) ]
+                  => apply UnderLets.nat_rect_interp_related
+                | [ |- UnderLets.interp_related _ _ (nat_rect _ _ _ _ _) (nat_rect _ _ _ _ _) ]
+                  => eapply UnderLets.nat_rect_arrow_interp_related; [ .. | eassumption ]
+                | [ |- UnderLets.interp_related _ _ (UnderLets.splice _ _) _ ]
+                  => rewrite UnderLets.splice_interp_related_iff
+                | [ |- UnderLets.interp_related ?ident_interp _ (UnderLets.splice_list _ _) _ ]
+                  => apply UnderLets.splice_list_interp_related_of_ex with (RA:=expr.interp_related ident_interp); exists (fun x => x); eexists; repeat apply conj; [ | | reflexivity ]
+                | [ H : UnderLets.interp_related _ _ ?e ?v1 |- UnderLets.interp_related _ _ ?e ?f ]
+                  => let f := match (eval pattern v1 in f) with ?f _ => f end in
+                     eapply (@UnderLets.interp_related_Proper_impl_same_UnderLets _ _ _ _ _ _ _ _ _ e v1 f); [ | exact H ]; cbv beta
+                | [ H : forall x y, ?R x y -> UnderLets.interp_related _ _ (?e x) (?v1 y) |- UnderLets.interp_related _ _ (?e ?xv) ?f ]
+                  => lazymatch f with
+                     | context[v1 ?yv]
+                       => let f := match (eval pattern (v1 yv) in f) with ?f _ => f end in
+                          eapply (@UnderLets.interp_related_Proper_impl_same_UnderLets _ _ _ _ _ _ _ _ _ (e xv) (v1 yv) f); [ | eapply H; assumption ]
+                     end
+                | [ |- expr.interp_related
+                         _
+                         (#(ident.prod_rect) @ ?f @ ?e)%expr
+                         match ?e' with pair a b => @?f' a b end ]
+                  => let fh := fresh in
+                     let eh := fresh in
+                     set (fh := f); set (eh := e); cbn [expr.interp_related]; subst fh eh;
+                     exists (fun ev => match ev with pair a b => f' a b end), e';
+                     repeat apply conj;
+                     [ | assumption | reflexivity ];
+                     exists (fun fv ev => match ev with pair a b => fv a b end), f';
+                     repeat apply conj;
+                     [ cbn [type.interp type.related ident_interp]; cbv [respectful]; intros; subst; eta_expand; auto | | reflexivity ]
+                | [ |- expr.interp_related
+                         _
+                         (#(ident.bool_rect) @ ?t @ ?f @ ?b)%expr
+                         (bool_rect ?P ?t' ?f' ?b') ]
+                  => let th := fresh in
+                     let fh := fresh in
+                     let bh := fresh in
+                     set (th := t); set (fh := f); set (bh := b); cbn [expr.interp_related]; subst th fh bh;
+                     unshelve
+                       ((exists (bool_rect P t' f'), b'); repeat apply conj;
+                        [ | shelve | reflexivity ];
+                        (exists (fun fv => bool_rect P t' (fv tt)), (fun _ => f')); repeat apply conj;
+                        [ | shelve | reflexivity ];
+                        (exists (fun tv fv => bool_rect P (tv tt) (fv tt)), (fun _ => t')); repeat apply conj;
+                        [ | shelve | reflexivity ])
+                | [ |- @expr.interp_related _ _ _ _ (type.base ?t) _ _ ]
+                  => lazymatch t with
+                     | base.type.type_base base.type.Z => idtac
+                     | base.type.prod (base.type.type_base base.type.Z) (base.type.type_base base.type.Z) => idtac
+                     end;
+                     progress repeat recurse_interp_related_step
+                | [ |- exists (fv : ?T1 -> ?T2) (ev : ?T1),
+                      _ /\ _ /\ fv ev = ?x ]
+                  => lazymatch T1 with Z => idtac | (Z * Z)%type => idtac end;
+                     lazymatch T2 with Z => idtac | (Z * Z)%type => idtac end;
+                     progress repeat recurse_interp_related_step
+                | [ |- expr.interp_related _ (expr.Abs ?f) _ ]
+                  => let fh := fresh in set (fh := f); cbn [expr.interp_related]; subst fh
+                | [ H : expr.interp_related _ ?x ?x' |- expr.interp_related _ (?f @ ?x) (?f' ?x') ]
+                  => let fh := fresh in
+                     let xh := fresh in
+                     set (fh := f); set (xh := x); cbn [expr.interp_related]; subst fh xh;
+                     exists f', x'; repeat apply conj;
+                     [ | exact H | reflexivity ]
+                | [ |- List.Forall2 _ (update_nth _ _ _) (update_nth _ _ _) ] => apply Forall2_update_nth
                 | [ H : context[ZRange.normalize (ZRange.normalize _)] |- _ ]
                   => rewrite ZRange.normalize_idempotent in H
                 | [ |- context[ZRange.normalize (ZRange.normalize _)] ]
@@ -338,6 +485,7 @@ Module Compilers.
                      [ clear -H; cbv [is_bounded_by_bool] in H; cbn [lower upper] in H; Bool.split_andb; Z.ltb_to_lt; lia..
                      | ]
                 end
+              | progress cbn [expr.interp_related] in *
               | match goal with
                 | [ H : context[expr.interp _ (UnderLets.interp _ (?f _ _ _))]
                     |- expr.interp _ (UnderLets.interp _ (?f _ _ _)) = _ ]
@@ -384,13 +532,19 @@ Module Compilers.
                   => tryif constr_eq x x' then fail else replace x with x' by lia
                 | [ |- _ = _ :> BinInt.Z ] => progress autorewrite with zsimplify_fast
                 | [ |- ident.cast _ ?r _ = ident.cast _ ?r _ ] => apply f_equal; Z.div_mod_to_quot_rem; nia
+                | [ H : forall x1 x2, ?R1 x1 x2 -> ?R2 (?f1 x1) (?f2 x2) |- ?R2 (?f1 _) (?f2 _) ]
+                  => apply H
+                | [ H : forall x1 x2, ?R1 x1 x2 -> forall y1 y2, ?R2 y1 y2 -> ?R3 (?f1 x1 y1) (?f2 x2 y2) |- ?R3 (?f1 _ _) (?f2 _ _) ]
+                  => apply H
+                | [ H : forall x x', ?Rx x x' -> forall y y', _ -> forall z z', ?Rz z z' -> ?R (?f x y z) (?f' x' y' z') |- ?R (?f _ _ _) (?f' _ _ _) ]
+                  => apply H; clear H
                 end ].
 
       Lemma nbe_rewrite_rules_interp_good
         : rewrite_rules_interp_goodT nbe_rewrite_rules.
       Proof using Type.
         Time start_interp_good.
-        Time all: repeat interp_good_t_step.
+        Time all: try solve [ repeat interp_good_t_step ].
       Qed.
 
       Lemma arith_rewrite_rules_interp_good max_const
@@ -438,66 +592,99 @@ Module Compilers.
         all: repeat first [ progress cbn [Compile.value' Compile.reify] in *
                           | progress subst
                           | match goal with
-                            | [ H : context[expr.interp ?ii ?v] |- _ ]
-                              => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
-                            | [ |- context[expr.interp ?ii ?v] ]
-                              => is_var v; generalize dependent (expr.interp ii v); clear v; intro v; intros
+                            | [ H : expr.interp_related _ ?x ?y |- _ ]
+                              => clear H x
                             end ].
         all: repeat match goal with
                     | [ H : _ = _ :> BinInt.Z |- _ ] => revert H
+                    | [ |- context[?v] ]
+                      => is_var v; match type of v with BinInt.Z => idtac end;
+                           revert v
+                    | [ v : BinInt.Z |- _ ] => clear v || revert v
+                    end.
+        all: repeat match goal with
+                    | [ |- forall n : BinInt.Z, _ ] => let x := fresh "xx" in intro x
+                    | [ |- forall n : _ = _ :> BinInt.Z, _ ] => let H := fresh "H" in intro H
+                    end.
+        all: repeat match goal with
+                    | [ H : _ = _ :> BinInt.Z |- _ ] => revert H
+                    | [ v : BinInt.Z |- _ ] => clear v || revert v
+                    end.
+        all: repeat match goal with
+                    | [ |- forall n : BinInt.Z, _ ] => let x := fresh "x" in intro x
+                    | [ |- forall n : _ = _ :> BinInt.Z, _ ] => let H := fresh "H" in intro H
+                    end.
+        all: repeat match goal with
+                    | [ H : _ = _ :> BinInt.Z |- _ ] => revert H
                     | [ v : BinInt.Z |- _ ] => clear v || revert v
                     end.
-        (* 16 subgoals (ID 105273)
+        Set Printing Width 80.
+        (* 16 subgoals (ID 124724)
 
   cast_outside_of_range : zrange -> Z -> Z
   invert_low, invert_high : Z -> Z -> option Z
-  Hlow : forall s v v' : Z, invert_low s v = Some v' -> v = Z.land v' (2 ^ (s / 2) - 1)
+  Hlow : forall s v v' : Z,
+         invert_low s v = Some v' -> v = Z.land v' (2 ^ (s / 2) - 1)
   Hhigh : forall s v v' : Z, invert_high s v = Some v' -> v = Z.shiftr v' (s / 2)
   ============================
-  forall x x0 v1 v0 : Z,
-  x = 2 ^ Z.log2 x -> (v1 + Z.shiftl v0 x0 mod x) / x = (v1 + Z.shiftl v0 x0) / x
+  forall x x0 x1 x2 : Z,
+  x2 = 2 ^ Z.log2 x2 ->
+  (x1 + Z.shiftl x0 x mod x2) / x2 = (x1 + Z.shiftl x0 x) / x2
 
-subgoal 2 (ID 105283) is:
- forall x x0 v0 v1 : Z,
- x = 2 ^ Z.log2 x -> (v0 + Z.shiftl v1 x0 mod x) / x = (Z.shiftl v1 x0 + v0) / x
-subgoal 3 (ID 105293) is:
- forall x x0 v1 v0 : Z,
- x = 2 ^ Z.log2 x -> (v1 + Z.shiftr v0 x0 mod x) / x = (v1 + Z.shiftr v0 x0) / x
-subgoal 4 (ID 105303) is:
- forall x x0 v0 v1 : Z,
- x = 2 ^ Z.log2 x -> (v0 + Z.shiftr v1 x0 mod x) / x = (Z.shiftr v1 x0 + v0) / x
-subgoal 5 (ID 105311) is:
- forall x v1 v0 : Z, x = 2 ^ Z.log2 x -> (v1 + v0 mod x) / x = (v1 + v0) / x
-subgoal 6 (ID 105323) is:
- forall x x0 v1 v0 v4 : Z,
- x = 2 ^ Z.log2 x -> (v1 + v0 + Z.shiftl v4 x0 mod x) / x = (v1 + v0 + Z.shiftl v4 x0) / x
-subgoal 7 (ID 105335) is:
- forall x x0 v1 v4 v0 : Z,
- x = 2 ^ Z.log2 x -> (v1 + v4 + Z.shiftl v0 x0 mod x) / x = (v1 + Z.shiftl v0 x0 + v4) / x
-subgoal 8 (ID 105347) is:
- forall x x0 v1 v0 v4 : Z,
- x = 2 ^ Z.log2 x -> (v1 + v0 + Z.shiftr v4 x0 mod x) / x = (v1 + v0 + Z.shiftr v4 x0) / x
-subgoal 9 (ID 105359) is:
- forall x x0 v1 v4 v0 : Z,
- x = 2 ^ Z.log2 x -> (v1 + v4 + Z.shiftr v0 x0 mod x) / x = (v1 + Z.shiftr v0 x0 + v4) / x
-subgoal 10 (ID 105369) is:
- forall x v1 v0 v4 : Z, x = 2 ^ Z.log2 x -> (v1 + v0 + v4 mod x) / x = (v1 + v0 + v4) / x
-subgoal 11 (ID 105379) is:
- forall x x0 v1 v0 : Z,
- x = 2 ^ Z.log2 x -> (v1 - Z.shiftl v0 x0 mod x) / x = (v1 - Z.shiftl v0 x0) / x
-subgoal 12 (ID 105389) is:
- forall x x0 v1 v0 : Z,
- x = 2 ^ Z.log2 x -> (v1 - Z.shiftr v0 x0 mod x) / x = (v1 - Z.shiftr v0 x0) / x
-subgoal 13 (ID 105397) is:
- forall x v1 v0 : Z, x = 2 ^ Z.log2 x -> (v1 - v0 mod x) / x = (v1 - v0) / x
-subgoal 14 (ID 105409) is:
- forall x x0 v1 v0 v4 : Z,
- x = 2 ^ Z.log2 x -> (v0 - Z.shiftl v4 x0 mod x - v1) / x = (v0 - Z.shiftl v4 x0 - v1) / x
-subgoal 15 (ID 105421) is:
- forall x x0 v1 v0 v4 : Z,
- x = 2 ^ Z.log2 x -> (v0 - Z.shiftr v4 x0 mod x - v1) / x = (v0 - Z.shiftr v4 x0 - v1) / x
-subgoal 16 (ID 105431) is:
- forall x v1 v0 v4 : Z, x = 2 ^ Z.log2 x -> (v0 - v4 mod x - v1) / x = (v0 - v4 - v1) / x
+subgoal 2 (ID 124734) is:
+ forall x x0 x1 x2 : Z,
+ x2 = 2 ^ Z.log2 x2 ->
+ (x1 + Z.shiftl x0 x mod x2) / x2 = (Z.shiftl x0 x + x1) / x2
+subgoal 3 (ID 124744) is:
+ forall x x0 x1 x2 : Z,
+ x2 = 2 ^ Z.log2 x2 ->
+ (x1 + Z.shiftr x0 x mod x2) / x2 = (x1 + Z.shiftr x0 x) / x2
+subgoal 4 (ID 124754) is:
+ forall x x0 x1 x2 : Z,
+ x2 = 2 ^ Z.log2 x2 ->
+ (x1 + Z.shiftr x0 x mod x2) / x2 = (Z.shiftr x0 x + x1) / x2
+subgoal 5 (ID 124762) is:
+ forall x x0 x1 : Z, x1 = 2 ^ Z.log2 x1 -> (x0 + x mod x1) / x1 = (x0 + x) / x1
+subgoal 6 (ID 124774) is:
+ forall x x0 x1 x2 x3 : Z,
+ x3 = 2 ^ Z.log2 x3 ->
+ (x2 + x1 + Z.shiftl x0 x mod x3) / x3 = (x2 + x1 + Z.shiftl x0 x) / x3
+subgoal 7 (ID 124786) is:
+ forall x x0 x1 x2 x3 : Z,
+ x3 = 2 ^ Z.log2 x3 ->
+ (x2 + x1 + Z.shiftl x0 x mod x3) / x3 = (x2 + Z.shiftl x0 x + x1) / x3
+subgoal 8 (ID 124798) is:
+ forall x x0 x1 x2 x3 : Z,
+ x3 = 2 ^ Z.log2 x3 ->
+ (x2 + x1 + Z.shiftr x0 x mod x3) / x3 = (x2 + x1 + Z.shiftr x0 x) / x3
+subgoal 9 (ID 124810) is:
+ forall x x0 x1 x2 x3 : Z,
+ x3 = 2 ^ Z.log2 x3 ->
+ (x2 + x1 + Z.shiftr x0 x mod x3) / x3 = (x2 + Z.shiftr x0 x + x1) / x3
+subgoal 10 (ID 124820) is:
+ forall x x0 x1 x2 : Z,
+ x2 = 2 ^ Z.log2 x2 -> (x1 + x0 + x mod x2) / x2 = (x1 + x0 + x) / x2
+subgoal 11 (ID 124830) is:
+ forall x x0 x1 x2 : Z,
+ x2 = 2 ^ Z.log2 x2 ->
+ (x1 - Z.shiftl x0 x mod x2) / x2 = (x1 - Z.shiftl x0 x) / x2
+subgoal 12 (ID 124840) is:
+ forall x x0 x1 x2 : Z,
+ x2 = 2 ^ Z.log2 x2 ->
+ (x1 - Z.shiftr x0 x mod x2) / x2 = (x1 - Z.shiftr x0 x) / x2
+subgoal 13 (ID 124848) is:
+ forall x x0 x1 : Z, x1 = 2 ^ Z.log2 x1 -> (x0 - x mod x1) / x1 = (x0 - x) / x1
+subgoal 14 (ID 124860) is:
+ forall x x0 x1 x2 x3 : Z,
+ x3 = 2 ^ Z.log2 x3 ->
+ (x2 - Z.shiftl x1 x0 mod x3 - x) / x3 = (x2 - Z.shiftl x1 x0 - x) / x3
+subgoal 15 (ID 124872) is:
+ forall x x0 x1 x2 x3 : Z,
+ x3 = 2 ^ Z.log2 x3 ->
+ (x2 - Z.shiftr x1 x0 mod x3 - x) / x3 = (x2 - Z.shiftr x1 x0 - x) / x3
+subgoal 16 (ID 124882) is:
+ forall x x0 x1 x2 : Z,
+ x2 = 2 ^ Z.log2 x2 -> (x1 - x0 mod x2 - x) / x2 = (x1 - x0 - x) / x2
          *)
         1-16: exact admit.
       Qed.
diff --git a/src/Experiments/NewPipeline/RewriterWf1.v b/src/Experiments/NewPipeline/RewriterWf1.v
index b69dd0fc4..6527e7a47 100644
--- a/src/Experiments/NewPipeline/RewriterWf1.v
+++ b/src/Experiments/NewPipeline/RewriterWf1.v
@@ -749,8 +749,12 @@ Module Compilers.
         Local Notation reveal_rawexpr e := (@reveal_rawexpr_cps ident _ e _ id).
         Local Notation unify_pattern' var := (@unify_pattern' ident var pident pident_arg_types pident_unify pident_unify_unknown).
         Local Notation unify_pattern var := (@unify_pattern ident var pident pident_arg_types pident_unify pident_unify_unknown).
-        Local Notation app_transport_with_unification_resultT'_cps var := (@app_transport_with_unification_resultT'_cps ident var pident pident_arg_types).
-        Local Notation app_with_unification_resultT_cps var := (@app_with_unification_resultT_cps ident var pident pident_arg_types type_vars_of_pident).
+        Local Notation app_transport_with_unification_resultT'_cps := (@app_transport_with_unification_resultT'_cps pident pident_arg_types).
+        Local Notation app_with_unification_resultT_cps := (@app_with_unification_resultT_cps pident pident_arg_types type_vars_of_pident).
+        Local Notation with_unification_resultT' := (@with_unification_resultT' pident pident_arg_types).
+        Local Notation with_unification_resultT := (@with_unification_resultT pident pident_arg_types type_vars_of_pident).
+        Local Notation unification_resultT' := (@unification_resultT' pident pident_arg_types).
+        Local Notation unification_resultT := (@unification_resultT pident pident_arg_types).
 
         Definition lam_type_of_list {ls K} : (type_of_list ls -> K) -> type_of_list_cps K ls
           := list_rect
@@ -1183,7 +1187,7 @@ Module Compilers.
                               | progress cbn [Option.bind with_unification_resultT' unification_resultT'] in *
                               | progress subst
                               | reflexivity
-                              | progress fold (@with_unification_resultT' ident var pident pident_arg_types)
+                              | progress fold (@with_unification_resultT' var)
                               | progress inversion_option
                               | break_innermost_match_step
                               | match goal with
@@ -1355,14 +1359,6 @@ Module Compilers.
           Local Notation rewrite_rulesT2 := (@rewrite_rulesT ident var2 pident pident_arg_types type_vars_of_pident).
           Local Notation eval_rewrite_rules1 := (@eval_rewrite_rules ident var1 pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple).
           Local Notation eval_rewrite_rules2 := (@eval_rewrite_rules ident var2 pident pident_arg_types pident_unify pident_unify_unknown raw_pident type_vars_of_pident full_types invert_bind_args invert_bind_args_unknown type_of_raw_pident raw_pident_to_typed raw_pident_is_simple).
-          Local Notation with_unification_resultT'1 := (@with_unification_resultT' ident var1 pident pident_arg_types).
-          Local Notation with_unification_resultT'2 := (@with_unification_resultT' ident var2 pident pident_arg_types).
-          Local Notation with_unification_resultT1 := (@with_unification_resultT ident var1 pident pident_arg_types type_vars_of_pident).
-          Local Notation with_unification_resultT2 := (@with_unification_resultT ident var2 pident pident_arg_types type_vars_of_pident).
-          Local Notation unification_resultT'1 := (@unification_resultT' ident var1 pident pident_arg_types).
-          Local Notation unification_resultT'2 := (@unification_resultT' ident var2 pident pident_arg_types).
-          Local Notation unification_resultT1 := (@unification_resultT ident var1 pident pident_arg_types).
-          Local Notation unification_resultT2 := (@unification_resultT ident var2 pident pident_arg_types).
           Local Notation rewrite_rule_data1 := (@rewrite_rule_data ident var1 pident pident_arg_types type_vars_of_pident).
           Local Notation rewrite_rule_data2 := (@rewrite_rule_data ident var2 pident pident_arg_types type_vars_of_pident).
           Local Notation with_unif_rewrite_ruleTP_gen1 := (@with_unif_rewrite_ruleTP_gen ident var1 pident pident_arg_types type_vars_of_pident).
@@ -1572,49 +1568,49 @@ Module Compilers.
             erewrite wf_unify_types by eassumption; reflexivity.
           Qed.
 
-          Fixpoint related_unification_resultT' (R : forall t, @value var1 t -> @value var2 t -> Prop) {t p evm}
-            : @unification_resultT'1 t p evm -> @unification_resultT'2 t p evm -> Prop
-            := match p return unification_resultT'1 p evm -> unification_resultT'2 p evm -> Prop with
+          Fixpoint related_unification_resultT' {var1 var2} (R : forall t, var1 t -> var2 t -> Prop) {t p evm}
+            : @unification_resultT' var1 t p evm -> @unification_resultT' var2 t p evm -> Prop
+            := match p in pattern.pattern t return @unification_resultT' var1 t p evm -> @unification_resultT' var2 t p evm -> Prop with
                | pattern.Wildcard t => R _
                | pattern.Ident t idc => eq
                | pattern.App s d f x
-                 => fun (v1 : unification_resultT'1 f evm * unification_resultT'1 x evm)
-                        (v2 : unification_resultT'2 f evm * unification_resultT'2 x evm)
-                    => @related_unification_resultT' R _ _ _ (fst v1) (fst v2)
-                       /\ @related_unification_resultT' R  _ _ _ (snd v1) (snd v2)
+                 => fun (v1 : unification_resultT' f evm * unification_resultT' x evm)
+                        (v2 : unification_resultT' f evm * unification_resultT' x evm)
+                    => @related_unification_resultT' _ _ R _ _ _ (fst v1) (fst v2)
+                       /\ @related_unification_resultT' _ _ R _ _ _ (snd v1) (snd v2)
                end.
 
           Definition wf_unification_resultT' (G : list {t1 : type & (var1 t1 * var2 t1)%type}) {t p evm}
-            : @unification_resultT'1 t p evm -> @unification_resultT'2 t p evm -> Prop
-            := @related_unification_resultT' (fun _ => wf_value G) t p evm.
+            : @unification_resultT' value t p evm -> @unification_resultT' value t p evm -> Prop
+            := @related_unification_resultT' _ _ (fun _ => wf_value G) t p evm.
 
-          Definition related_unification_resultT (R : forall t, @value var1 t -> @value var2 t -> Prop) {t p}
-            : @unification_resultT1 t p -> @unification_resultT2 t p -> Prop
-            := related_sigT_by_eq (@related_unification_resultT' R t p).
+          Definition related_unification_resultT {var1 var2} (R : forall t, var1 t -> var2 t -> Prop) {t p}
+            : @unification_resultT _ t p -> @unification_resultT _ t p -> Prop
+            := related_sigT_by_eq (@related_unification_resultT' _ _ R t p).
 
           Definition wf_unification_resultT (G : list {t1 : type & (var1 t1 * var2 t1)%type}) {t p}
-            : @unification_resultT1 t p -> @unification_resultT2 t p -> Prop
-            := @related_unification_resultT (fun _ => wf_value G) t p.
+            : @unification_resultT (@value var1) t p -> @unification_resultT (@value var2) t p -> Prop
+            := @related_unification_resultT _ _ (fun _ => wf_value G) t p.
 
-          Fixpoint under_with_unification_resultT'_relation_hetero {t p evm K1 K2}
-                   (FH : forall t, value t -> value t -> Prop)
+          Fixpoint under_with_unification_resultT'_relation_hetero {var1 var2 t p evm K1 K2}
+                   (FH : forall t, var1 t -> var2 t -> Prop)
                    (F : K1 -> K2 -> Prop)
                    {struct p}
-            : @with_unification_resultT'1 t p evm K1 -> @with_unification_resultT'2 t p evm K2 -> Prop
-            := match p return with_unification_resultT'1 p evm K1 -> with_unification_resultT'2 p evm K2 -> Prop with
+            : @with_unification_resultT' var1 t p evm K1 -> @with_unification_resultT' var2 t p evm K2 -> Prop
+            := match p in pattern.pattern t return @with_unification_resultT' var1 t p evm K1 -> @with_unification_resultT' var2 t p evm K2 -> Prop with
                | pattern.Wildcard t => fun f1 f2 => forall v1 v2, FH _ v1 v2 -> F (f1 v1) (f2 v2)
                | pattern.Ident t idc => under_type_of_list_relation_cps F
                | pattern.App s d f x
                  => @under_with_unification_resultT'_relation_hetero
-                      _ f evm _ _
+                      _ _ _ f evm _ _
                       FH
-                      (@under_with_unification_resultT'_relation_hetero _ x evm _ _ FH F)
+                      (@under_with_unification_resultT'_relation_hetero _ _ _ x evm _ _ FH F)
                end.
 
-          Definition under_with_unification_resultT_relation_hetero {t p K1 K2}
-                     (FH : forall t, value t -> value t -> Prop)
+          Definition under_with_unification_resultT_relation_hetero {var1 var2 t p K1 K2}
+                     (FH : forall t, var1 t -> var2 t -> Prop)
                      (F : forall evm, K1 (pattern.type.subst_default t evm) -> K2 (pattern.type.subst_default t evm) -> Prop)
-            : @with_unification_resultT1 t p K1 -> @with_unification_resultT2 t p K2 -> Prop
+            : @with_unification_resultT var1 t p K1 -> @with_unification_resultT var2 t p K2 -> Prop
             := pattern.type.under_forall_vars_relation
                  (fun evm => under_with_unification_resultT'_relation_hetero FH (F evm)).
 
@@ -1622,19 +1618,19 @@ Module Compilers.
                      (G : list {t : _ & (var1 t * var2 t)%type})
                      {t} {p : pattern t} {K1 K2 : type -> Type}
                      (P : forall evm, K1 (pattern.type.subst_default t evm) -> K2 (pattern.type.subst_default t evm) -> Prop)
-            : @with_unification_resultT1 t p K1 -> @with_unification_resultT2 t p K2 -> Prop
+            : @with_unification_resultT value t p K1 -> @with_unification_resultT value t p K2 -> Prop
             := under_with_unification_resultT_relation_hetero
                  (fun t => wf_value G)
                  P.
 
-          Lemma related_app_with_unification_resultT' {t p evm K1 K2}
+          Lemma related_app_with_unification_resultT' {var1' var2' t p evm K1 K2}
                 R1 R2
                 f1 f2 v1 v2
             : @under_with_unification_resultT'_relation_hetero
-                t p evm K1 K2 R1 R2 f1 f2
-              -> @related_unification_resultT' R1 t p evm v1 v2
-              -> R2 (@app_with_unification_resultT' _ _ _ _ t p evm K1 f1 v1)
-                    (@app_with_unification_resultT' _ _ _ _ t p evm K2 f2 v2).
+                var1' var2' t p evm K1 K2 R1 R2 f1 f2
+              -> @related_unification_resultT' var1' var2' R1 t p evm v1 v2
+              -> R2 (@app_with_unification_resultT' _ _ _ t p evm K1 f1 v1)
+                    (@app_with_unification_resultT' _ _ _ t p evm K2 f2 v2).
           Proof using Type.
             revert K1 K2 R1 R2 f1 f2 v1 v2; induction p; cbn in *; intros; subst; destruct_head'_and;
               try apply related_app_type_of_list_of_under_type_of_list_relation_cps;
@@ -1642,12 +1638,12 @@ Module Compilers.
             repeat match goal with H : _ |- _ => eapply H; eauto; clear H end.
           Qed.
 
-          Lemma related_app_transport_with_unification_resultT' {t p evm1 evm2 K1 K2}
+          Lemma related_app_transport_with_unification_resultT' {var1' var2' t p evm1 evm2 K1 K2}
                 R1 R2
                 f1 f2 v1 v2
             : @under_with_unification_resultT'_relation_hetero
-                t p evm1 K1 K2 R1 R2 f1 f2
-              -> @related_unification_resultT' R1 t p evm2 v1 v2
+                var1' var2' t p evm1 K1 K2 R1 R2 f1 f2
+              -> @related_unification_resultT' var1' var2' R1 t p evm2 v1 v2
               -> option_eq
                    R2
                    (@app_transport_with_unification_resultT'_cps _ t p evm1 evm2 K1 f1 v1 _ (@Some _))
@@ -1661,14 +1657,14 @@ Module Compilers.
                               | break_innermost_match_step
                               | reflexivity
                               | progress cbn [Option.bind option_eq] in *
-                              | progress fold (@with_unification_resultT'1) (@with_unification_resultT'2)
+                              | progress fold (@with_unification_resultT')
                               | progress cps_id'_with_option app_transport_with_unification_resultT'_cps_id
                               | progress cbv [eq_rect]
                               | solve [ auto ]
                               | exfalso; assumption
                               | progress inversion_option
                               | match goal with
-                                | [ H : (forall K1 K2 R1 R2 (f1 : with_unification_resultT'1 ?p1 ?evm1 K1), _)
+                                | [ H : (forall K1 K2 R1 R2 (f1 : with_unification_resultT' ?p1 ?evm1 K1), _)
                                     |- context[@app_transport_with_unification_resultT'_cps _ ?t ?p1 ?evm1 ?evm2 ?K1' ?f1' ?v1' _ _] ]
                                   => specialize (H K1' _ _ _ f1' _ v1' _ ltac:(eassumption) ltac:(eassumption))
                                 | [ H : option_eq ?R ?x ?y |- _ ]
@@ -1676,12 +1672,12 @@ Module Compilers.
                                 end ].
           Qed.
 
-          Lemma related_app_with_unification_resultT {t p K1 K2}
+          Lemma related_app_with_unification_resultT {var1' var2' t p K1 K2}
                 R1 R2
                 f1 f2 v1 v2
             : @under_with_unification_resultT_relation_hetero
-                t p K1 K2 R1 R2 f1 f2
-              -> @related_unification_resultT R1 t p v1 v2
+                var1' var2' t p K1 K2 R1 R2 f1 f2
+              -> @related_unification_resultT var1' var2' R1 t p v1 v2
               -> option_eq
                    (related_sigT_by_eq R2)
                    (@app_with_unification_resultT_cps _ t p K1 f1 v1 _ (@Some _))
@@ -1723,20 +1719,20 @@ Module Compilers.
                    (@app_with_unification_resultT_cps _ t p K2 f2 v2 _ (@Some _)).
           Proof using Type. apply related_app_with_unification_resultT. Qed.
 
-          Definition map_related_unification_resultT' {R1 R2 : forall t : type, value t -> value t -> Prop}
+          Definition map_related_unification_resultT' {var1' var2'} {R1 R2 : forall t : type, var1' t -> var2' t -> Prop}
                      (HR : forall t v1 v2, R1 t v1 v2 -> R2 t v1 v2)
                      {t p evm v1 v2}
-            : @related_unification_resultT' R1 t p evm v1 v2
-              -> @related_unification_resultT' R2 t p evm v1 v2.
+            : @related_unification_resultT' var1' var2' R1 t p evm v1 v2
+              -> @related_unification_resultT' var1' var2' R2 t p evm v1 v2.
           Proof using Type.
             induction p; cbn [related_unification_resultT']; intuition auto.
           Qed.
 
-          Definition map_related_unification_resultT {R1 R2 : forall t : type, value t -> value t -> Prop}
+          Definition map_related_unification_resultT {var1' var2'} {R1 R2 : forall t : type, var1' t -> var2' t -> Prop}
                      (HR : forall t v1 v2, R1 t v1 v2 -> R2 t v1 v2)
                      {t p v1 v2}
-            : @related_unification_resultT R1 t p v1 v2
-              -> @related_unification_resultT R2 t p v1 v2.
+            : @related_unification_resultT var1' var2' R1 t p v1 v2
+              -> @related_unification_resultT var1' var2' R2 t p v1 v2.
           Proof using Type.
             cbv [related_unification_resultT]; apply map_related_sigT_by_eq; intros *.
             apply map_related_unification_resultT'; auto.
@@ -1820,8 +1816,8 @@ Module Compilers.
                              (gy : { evm : _ & deep_rewrite_ruleTP_gen2 rew_should_do_again2 rew_with_opt2 rew_under_lets2 _ })
                          => related_sigT_by_eq
                               (fun _ => wf_deep_rewrite_ruleTP_gen G) fx gy)
-                        (app_with_unification_resultT_cps _ f x _ (@Some _))
-                        (app_with_unification_resultT_cps _ g y _ (@Some _)).
+                        (app_with_unification_resultT_cps f x _ (@Some _))
+                        (app_with_unification_resultT_cps g y _ (@Some _)).
 
           Definition wf_rewrite_rule_data
                      (G : list {t : _ & (var1 t * var2 t)%type})
@@ -1911,7 +1907,6 @@ Module Compilers.
           Local Notation rewrite_rulesT := (@rewrite_rulesT ident var pident pident_arg_types type_vars_of_pident).
           Local Notation rewrite_rule_data := (@rewrite_rule_data ident var pident pident_arg_types type_vars_of_pident).
           Local Notation with_unif_rewrite_ruleTP_gen := (@with_unif_rewrite_ruleTP_gen ident var pident pident_arg_types type_vars_of_pident).
-          Local Notation with_unification_resultT' := (@with_unification_resultT' ident var pident pident_arg_types).
           Local Notation normalize_deep_rewrite_rule := (@normalize_deep_rewrite_rule ident var).
 
           Local Notation deep_rewrite_ruleTP_gen := (@deep_rewrite_ruleTP_gen ident var).
@@ -1930,133 +1925,52 @@ Module Compilers.
             : var t
             := expr.interp ident_interp (reify v).
 
-          Fixpoint value'_interp_related
-                   {with_lets1 with_lets2 t}
-            : @value' var with_lets1 t
-              -> @value' var with_lets2 t
-              -> Prop
-            := match t return value' _ t -> value' _ t -> Prop with
-               | type.base t
-                 => fun v1 v2
-                    => expr.interp ident_interp (UnderLets_maybe_interp with_lets1 v1)
-                       == expr.interp ident_interp (UnderLets_maybe_interp with_lets2 v2)
-               | type.arrow s d
-                 => fun (f1 f2 : value' _ s -> value' _ d)
+          Local Notation expr_interp_related := (@expr.interp_related _ ident _ ident_interp).
+          Local Notation UnderLets_interp_related := (@UnderLets.interp_related _ ident _ ident_interp _ _ expr_interp_related).
+
+          Fixpoint value_interp_related {t with_lets} : @value' var with_lets t -> type.interp base.interp t -> Prop
+            := match t, with_lets with
+               | type.base _, true => UnderLets_interp_related
+               | type.base _, false => expr_interp_related
+               | type.arrow s d, _
+                 => fun (f1 : @value' _ _ s -> @value' _ _ d) (f2 : type.interp _ s -> type.interp _ d)
                     => forall x1 x2,
-                        @value'_interp_related _ _ s x1 x2
-                        -> @value'_interp_related _ _ d (f1 x1) (f2 x2)
+                        @value_interp_related s _ x1 x2
+                        -> @value_interp_related d _ (f1 x1) (f2 x2)
                end.
 
-          Local Infix "===" := value'_interp_related : type_scope.
-          Local Notation "e1 ==== e2" := (existT expr _ e1 = existT expr _ e2) : type_scope.
-
-          Definition value_interp_related {t} : relation (@value var t)
-            := value'_interp_related.
-
-          Definition value_interp_ok {with_lets t} : @value' var with_lets t -> Prop
-            := fun v => value'_interp_related v v.
-
-          Local Notation G_good G
-            := (forall t v1 v2, List.In (existT (fun t => (var t * var t)%type) t (v1, v2)) G -> v1 == v2)
-                 (only parsing).
-
-          Definition value_or_expr_interp_ok {with_lets t} : @value' var with_lets t -> Prop
-            := match t with
-               | type.base _
-                 => fun v => exists G, G_good G /\ UnderLets_maybe_wf with_lets G v v
-               | type.arrow _ _
-                 => value_interp_ok
+          Fixpoint rawexpr_interp_related (r1 : rawexpr) : type.interp base.interp (type_of_rawexpr r1) -> Prop
+            := match r1 return type.interp base.interp (type_of_rawexpr r1) -> Prop with
+               | rExpr _ e1
+               | rValue (type.base _) e1
+                 => expr_interp_related e1
+               | rValue t1 v1
+                 => value_interp_related v1
+               | rIdent _ t1 idc1 t'1 alt1
+                 => fun v2
+                    => expr.interp ident_interp alt1 == v2
+                       /\ existT expr t1 (expr.Ident idc1) = existT expr t'1 alt1
+               | rApp f1 x1 t1 alt1
+                 => match alt1 in expr.expr t return type.interp base.interp t -> Prop with
+                    | expr.App s d af ax
+                      => fun v2
+                         => exists fv xv (pff : type.arrow s d = type_of_rawexpr f1) (pfx : s = type_of_rawexpr x1),
+                             @expr_interp_related _ af fv
+                             /\ @expr_interp_related _ ax xv
+                             /\ @rawexpr_interp_related f1 (rew pff in fv)
+                             /\ @rawexpr_interp_related x1 (rew pfx in xv)
+                             /\ fv xv = v2
+                    | _ => fun _ => False
+                    end
                end.
 
-          Lemma value_interp_ok_of_value_or_expr_interp_ok {with_lets t v}
-            : @value_or_expr_interp_ok with_lets t v
-              -> value_interp_ok v.
-          Proof using ident_interp_Proper.
-            cbv [value_or_expr_interp_ok]; break_innermost_match; [ | | exact id ]; cbv [value_interp_ok value'_interp_related]; rewrite <- ?UnderLets.interp_to_expr.
-            all: intros [G [H1 H2] ].
-            all: eapply expr.wf_interp_Proper_gen1; try eassumption.
-            apply UnderLets.wf_to_expr; assumption.
-          Qed.
-
-          Lemma value'_interp_related_sym_iff {with_lets1 with_lets2 t v1 v2}
-            : @value'_interp_related with_lets1 with_lets2 t v1 v2
-              <-> @value'_interp_related with_lets2 with_lets1 t v2 v1.
-          Proof using Type.
-            split; revert with_lets1 with_lets2 v1 v2; induction t as [|s IHs d IHd];
-              cbn [value'_interp_related]; intros.
-            all: solve [ symmetry; assumption | eauto ].
-          Qed.
+          Definition unification_resultT'_interp_related {t p evm}
+            : @unification_resultT' (@value var) t p evm -> @unification_resultT' var t p evm -> Prop
+            := related_unification_resultT' (fun t => value_interp_related).
 
-          Lemma value'_interp_related_trans {with_lets1 with_lets2 with_lets3 t v1 v2 v3}
-            : @value'_interp_related with_lets1 with_lets2 t v1 v2
-              -> @value'_interp_related with_lets2 with_lets3 t v2 v3
-              -> @value'_interp_related with_lets1 with_lets3 t v1 v3.
-          Proof using Type.
-            intros H0 H1; revert with_lets1 with_lets2 with_lets3 v1 v2 v3 H0 H1; induction t as [|s IHs d IHd];
-              cbn [value'_interp_related]; intros.
-            all: try solve [ etransitivity; eassumption ].
-            eapply IHd; [ eapply H0; eassumption | eapply H1 ].
-            eapply IHs; [ eapply value'_interp_related_sym_iff | ]; eassumption.
-          Qed.
-
-          Global Instance value'_interp_related_Symmetric {with_lets t}
-            : Symmetric (@value'_interp_related with_lets with_lets t) | 10
-            := fun v1 v2 => proj1 value'_interp_related_sym_iff.
-          Global Instance value'_interp_related_Transitive {with_lets t}
-            : Transitive (@value'_interp_related with_lets with_lets t) | 10
-            := fun v1 v2 v3 => value'_interp_related_trans.
-
-          Lemma value_interp_related_sym_iff {t v1 v2}
-            : @value_interp_related t v1 v2
-              <-> @value_interp_related t v2 v1.
-          Proof using Type. apply value'_interp_related_sym_iff. Qed.
-
-          Lemma value_interp_related_trans {t v1 v2 v3}
-            : @value_interp_related t v1 v2
-              -> @value_interp_related t v2 v3
-              -> @value_interp_related t v1 v3.
-          Proof using Type. apply value'_interp_related_trans. Qed.
-
-          Global Instance value_interp_related_Symmetric {t}
-            : Symmetric (@value_interp_related t) | 10
-            := fun v1 v2 => proj1 value_interp_related_sym_iff.
-          Global Instance value_interp_related_Transitive {t}
-            : Transitive (@value_interp_related t) | 10
-            := fun v1 v2 v3 => value_interp_related_trans.
-
-          Lemma interp_Base_value {with_lets2 t} v1 (v2 : value' with_lets2 t)
-            : v1 === v2 -> @Base_value var t v1 === v2.
-          Proof using Type.
-            cbv [Base_value]; break_innermost_match; destruct with_lets2; cbn [value'_interp_related UnderLets.interp];
-              exact id.
-          Qed.
-
-          Fixpoint value_interp_related_reify {with_lets1 with_lets2 t e1 e2} {struct t}
-            : e1 === e2
-              -> expr.interp ident_interp (@reify var with_lets1 t e1) == expr.interp ident_interp (@reify var with_lets2 t e2)
-          with value_interp_related_reflect {with_lets1 with_lets2 t e1 e2} {struct t}
-            : expr.interp ident_interp e1 == expr.interp ident_interp e2
-              -> @reflect var with_lets1 t e1 === @reflect var with_lets2 t e2.
-          Proof using Type.
-            all: destruct t as [t|s d];
-              [ clear value_interp_related_reflect value_interp_related_reify
-              | pose proof (fun with_lets1 with_lets2 => value_interp_related_reify with_lets1 with_lets2 s) as value_interp_related_reify_s;
-                pose proof (fun with_lets1 with_lets2 => value_interp_related_reify with_lets1 with_lets2 d) as value_interp_related_reify_d;
-                pose proof (fun with_lets1 with_lets2 => value_interp_related_reflect with_lets1 with_lets2 s) as value_interp_related_reflect_s;
-                pose proof (fun with_lets1 with_lets2 => value_interp_related_reflect with_lets1 with_lets2 d) as value_interp_related_reflect_d;
-                clear value_interp_related_reify value_interp_related_reflect ].
-
-            all: repeat first [ progress cbn [reflect reify type.related value'_interp_related expr.interp] in *
-                              | progress cbv [respectful]
-                              | progress fold (@reify) (@reflect) in *
-                              | break_innermost_match_step
-                              | rewrite UnderLets.interp_to_expr
-                              | exact id
-                              | progress intros
-                              | match goal with
-                                | [ H : _ |- _ ] => apply H; clear H
-                                end ].
-          Qed.
+          Definition unification_resultT_interp_related {t p}
+            : @unification_resultT (@value var) t p -> @unification_resultT var t p -> Prop
+            := related_unification_resultT (fun t => value_interp_related).
 
           Lemma interp_reify_reflect {with_lets t} e v
             : expr.interp ident_interp e == v -> expr.interp ident_interp (@reify _ with_lets t (reflect e)) == v.
@@ -2069,202 +1983,6 @@ Module Compilers.
             apply IHd; cbn [expr.interp]; auto.
           Qed.
 
-          Lemma interp_reflect_reify {with_lets with_lets1 with_lets2 t} x y
-            : @value'_interp_related with_lets with_lets2 t x y -> @value'_interp_related with_lets1 with_lets2 t (reflect (@reify _ with_lets t x)) y.
-          Proof using Type.
-            revert with_lets with_lets1 with_lets2 x y; induction t as [|s IHs d IHd]; intros ? ? ? ? ?;
-              cbn [type.related value'_interp_related reflect reify] in *;
-              fold (@reify var) (@reflect var); cbv [respectful]; break_innermost_match;
-                cbn [expr.interp UnderLets.to_expr UnderLets.interp]; rewrite ?UnderLets.interp_to_expr; auto; [].
-            intros Hf ? ? Hx.
-            etransitivity.
-            { eapply value_interp_related_reflect; cbn [expr.interp].
-              eapply value_interp_related_reify.
-              eapply Hf.
-              eapply value_interp_related_reflect; cbn [expr.interp].
-              eapply value_interp_related_reify; eassumption. }
-            { etransitivity; [ eapply IHd; symmetry | ]; eapply Hf; [ symmetry | eassumption ].
-              eapply IHs; symmetry; eassumption. }
-          Qed.
-
-          Lemma value_interp_related_of_ok {with_lets1 with_lets2 t v1 v2}
-            : @value'_interp_related with_lets1 with_lets2 t v1 v2
-              -> value'_interp v1 == value'_interp v2.
-          Proof using Type.
-            revert with_lets1 with_lets2 v1 v2; induction t as [|s IHs d IHd].
-            { cbn; intros; break_innermost_match; rewrite ?UnderLets.interp_to_expr; assumption. }
-            { cbn [type.related value'_interp value'_interp_related value']; cbv [respectful].
-              intros.
-              apply IHd; fold (@reify var) (@reflect var).
-              match goal with H : _ |- _ => apply H end.
-              apply value_interp_related_reflect; cbn [expr.interp]; assumption. }
-          Qed.
-
-          Local Ltac t_value_interp_related :=
-            repeat match goal with
-                   | _ => progress cbn [expr.interp]
-                   | [ |- expr.interp ?ii ?e == ?v ]
-                     => is_var v; is_evar e; refine (_ : expr.interp ii (expr.Var v) == v)
-                   | [ H : ?R ?x ?y |- ?R ?x ?x ]
-                     => etransitivity; (idtac + symmetry); eassumption
-                   | [ H : ?R ?y ?x |- ?R ?x ?x ]
-                     => etransitivity; (idtac + symmetry); eassumption
-                   | [ |- expr.interp _ (reify _) == expr.interp _ (reify _) ]
-                     => eapply value_interp_related_reify
-                   | [ |- reflect _ === reflect _ ]
-                     => eapply value_interp_related_reflect
-                   | [ |- reflect (expr.Var _) === _ ]
-                     => etransitivity; [ eapply value_interp_related_reflect | ]
-                   | [ |- _ === reflect (expr.Var _) ]
-                     => etransitivity; [ | eapply value_interp_related_reflect ]
-                   | [ |- _ === reflect ?v ]
-                     => is_evar v; symmetry; eapply interp_reflect_reify
-                   | [ |- reflect ?v === _ ]
-                     => is_evar v; eapply interp_reflect_reify
-                   | [ |- _ == expr.interp _ (reify ?v) ]
-                     => is_evar v; symmetry; eapply interp_reify_reflect
-                   | [ |- expr.interp _ (reify ?v) == _ ]
-                     => is_evar v; eapply interp_reify_reflect
-                   | [ |- expr.interp _ (reify ?x) == ?v ]
-                     => is_var x; is_evar v; eapply value_interp_related_reify
-                   | [ |- ?v == expr.interp _ (reify ?x) ]
-                     => is_var x; is_evar v; eapply value_interp_related_reify
-                   | [ |- expr.interp _ (reify ?x) == expr.interp _ ?v ]
-                     => is_var x; is_evar v; eapply value_interp_related_reify
-                   | [ |- expr.interp _ ?v == expr.interp _ (reify ?x) ]
-                     => is_var x; is_evar v; eapply value_interp_related_reify
-                   | [ H : forall x1 x2, x1 === x2 -> ?f1 x1 === ?f2 x2 |- ?f1 _ === _ ] => eapply H; clear H
-                   | [ H : (forall x1 x2, x1 === x2 -> ?f1 x1 === reflect (?f2 @ reify x2)%expr)
-                       |- ?f1 _ === reflect (?f2 @ reify _)%expr ]
-                     => eapply H; clear H
-                   | [ H : forall x y, x == y -> _ == expr.interp _ ?f2 y |- _ == expr.interp _ ?f2 _ ]
-                     => etransitivity; [ | eapply H ]; clear H
-                   | _ => (idtac + symmetry); eassumption
-                   end.
-
-          Lemma value_interp_related_reify_reflect_iff
-                {with_lets1 with_lets2 t v1 e2}
-                (v2 := reflect e2)
-            : @value_interp_ok with_lets1 t v1
-              -> expr.interp ident_interp e2 == expr.interp ident_interp e2
-              -> (@value'_interp_related with_lets1 with_lets2 t v1 v2
-                  <-> expr.interp ident_interp (reify v1) == expr.interp ident_interp e2).
-          Proof using Type.
-            subst v2; cbv [value_interp_ok] in *.
-            revert with_lets1 with_lets2 v1 e2.
-            induction t as [|s IHs d IHd]; cbn [value'_interp_related] in *.
-            { cbn; intros; break_innermost_match; rewrite ?UnderLets.interp_to_expr; reflexivity. }
-            { intros ? ? v1 e2 H1 H2.
-              cbn [type.related] in *; cbv [respectful] in *.
-              specialize (IHd true true); specialize (IHs false false).
-              cbn [reify reflect expr.interp] in *.
-              fold (@reify var) (@reflect var) in *.
-              cbn [value' expr.interp] in *.
-              specialize (fun x1 (x2 : value' false s) pf1 => IHd (v1 x1) (e2 @ reify x2)%expr (H1 _ _ pf1)); cbn [expr.interp] in *.
-              specialize (fun x1 x2 pf1 pf2 => IHd x1 x2 pf1 (H2 _ _ (value_interp_related_reify pf2))).
-              split; intros H ? ? H'; [ etransitivity; [ eapply IHd | eapply H2 ]; clear IHd | apply IHd; clear IHd ]; cbn [expr.interp] in *.
-              all: unshelve (t_value_interp_related; t_value_interp_related); trivial. }
-          Qed.
-
-          Lemma value_interp_related_iff_of_ok {t with_lets1 with_lets2 v1 v2}
-            : @value_interp_ok with_lets1 t v1
-              -> @value_interp_ok with_lets2 t v2
-              -> (@value'_interp_related with_lets1 with_lets2 t v1 v2
-                  <-> value'_interp v1 == value'_interp v2).
-          Proof using Type.
-            cbv [value_interp_ok value'_interp] in *.
-            intros H1 H2; split; intro H.
-            { eapply value_interp_related_reify_reflect_iff;
-                [ eassumption | eapply value_interp_related_reify | symmetry; eapply interp_reflect_reify ].
-              { etransitivity; (idtac + symmetry); eassumption. }
-              { eapply value'_interp_related_sym_iff; eassumption. } }
-            { eapply value_interp_related_reify_reflect_iff in H; [ | eassumption | ].
-              { eapply value'_interp_related_trans; [ eexact H | eapply interp_reflect_reify ].
-                etransitivity; (idtac + symmetry); eassumption. }
-              { eapply value_interp_related_reify.
-                etransitivity; (idtac + symmetry); eassumption. } }
-            Unshelve.
-            all: trivial.
-          Qed.
-
-          Lemma value'_interp_app {with_lets s d f x}
-            : @value_interp_ok with_lets (type.arrow s d) f
-              -> @value_interp_ok _ s x
-              -> value'_interp (f x) == value'_interp f (value'_interp x).
-          Proof using Type.
-            cbv [value_interp_ok]; cbn [value'_interp_related value'] in *.
-            intros Hf Hx.
-            transitivity (value'_interp (with_lets:=false) (t:=type.arrow s d) (fun x => f (reflect (reify x))) (value'_interp x)).
-            all: fold (@value' var).
-            { cbv [value'_interp]; cbn [reify reflect expr.interp].
-              fold (@reify var) (@reflect var).
-              eapply value_interp_related_iff_of_ok; apply Hf;
-                repeat first [ eassumption
-                             | progress cbn [expr.interp]
-                             | (idtac + symmetry); apply interp_reflect_reify
-                             | eapply value_interp_related_reflect
-                             | eapply value_interp_related_reify
-                             | etransitivity; [ eapply value_interp_related_reflect; progress cbn [expr.interp] | ] ]. }
-            { eapply (@value_interp_related_iff_of_ok (type.arrow s d));
-                fold (@type.related); cbv [value_interp_ok]; cbn [value'_interp_related];
-                  [ .. | eapply value_interp_related_iff_of_ok ]; try assumption.
-              all: intros; apply Hf.
-              all: repeat first [ (idtac + symmetry); apply interp_reflect_reify
-                                | (idtac + symmetry); assumption ]. }
-          Qed.
-
-          Lemma unfold_value'_interp_arrow {with_lets s d}
-            : @value'_interp with_lets (type.arrow s d)
-              = (fun (f : @value' _ with_lets (type.arrow s d)) (x : var s)
-                 => @value'_interp _ d (f (reflect (expr.Var x)))).
-          Proof using Type. reflexivity. Qed.
-
-          Lemma value_interp_self_related_of_ok {with_lets t v}
-            : @value_interp_ok with_lets t v
-              -> value'_interp v == value'_interp v.
-          Proof using Type.
-            intro H; apply value_interp_related_iff_of_ok; assumption.
-          Qed.
-
-          Lemma value_interp_ok_arrow {with_lets s d f}
-            : @value_interp_ok with_lets (type.arrow s d) f
-              <-> (forall x y,
-                      value_interp_ok x
-                      -> value_interp_ok y
-                      -> value'_interp x == value'_interp y
-                      -> value_interp_ok (f x)
-                         /\ value_interp_ok (f y)
-                         /\ value'_interp (f x) == value'_interp (f y)).
-          Proof using Type.
-            cbv [value_interp_ok]; cbn [value'_interp_related value'] in *.
-            split; intros H x y; [ | specialize (H x y) ].
-            all: repeat first [ progress intros
-                              | apply conj
-                              | progress destruct_head'_and
-                              | progress cbv [value_interp_ok] in *
-                              | solve [ auto ]
-                              | progress specialize_by_assumption
-                              | match goal with
-                                | [ H : (forall x1 x2, x1 === x2 -> ?f x1 === ?f x2) |- ?f _ === ?f _ ]
-                                  => apply H
-                                | [ |- _ == _ ] => rewrite <- value_interp_related_iff_of_ok
-                                | [ H : _ == _ |- _ ] => revert H; rewrite <- value_interp_related_iff_of_ok
-                                | [ H : ?x === ?y |- _ ]
-                                  => progress ((try unique assert (x === x) by (etransitivity; (idtac + symmetry); eassumption));
-                                               (try unique assert (y === y) by (etransitivity; (idtac + symmetry); eassumption)))
-                                | [ H : _ == _ -> _ |- _ ]
-                                  => specialize (fun H1 H2 H3 => H (proj1 (value_interp_related_iff_of_ok H1 H2) H3))
-                                end ].
-          Qed.
-
-          Lemma value_interp_ok_base {with_lets t x}
-            : @value_interp_ok with_lets (type.base t) x
-              <-> (value'_interp x == value'_interp x).
-          Proof using Type.
-            cbv [value'_interp value_interp_ok reify value'_interp_related].
-            break_innermost_match; rewrite ?UnderLets.interp_to_expr; reflexivity.
-          Qed.
-
           Lemma interp_of_wf_reify_expr G {t}
                 (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> expr.interp ident_interp (reify v1) == v2)
                 e1 e2
@@ -2286,137 +2004,57 @@ Module Compilers.
                               | solve [ auto ] ].
           Qed.
 
-          Fixpoint rawexpr_interp_ok (r : rawexpr) : Prop
-            := match r with
-               | rIdent _ t idc t' alt => expr.Ident idc ==== alt
-               | rExpr t e
-               | rValue (type.base t) e
-                 => exists G,
-                    (forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2)
-                    /\ expr.wf G e e
-               | rValue t v => value_interp_ok v
-               | rApp f x t alt
-                 => rawexpr_interp_ok f
-                    /\ rawexpr_interp_ok x
-                    /\ exists s d
-                              (pff : type_of_rawexpr f = type.arrow s d)
-                              (pfx : type_of_rawexpr x = s),
-                        (((rew pff in expr_of_rawexpr f) @ (rew pfx in expr_of_rawexpr x))%expr)
-                          ==== alt
-               end.
-
-          Lemma rawexpr_equiv_expr_ok_iff {t e r} (H : @rawexpr_equiv_expr _ t e r)
-            : rawexpr_interp_ok r
-              <-> (exists G,
-                      (forall t v1 v2, List.In (existT _ t (v1, v2)) G -> v1 == v2)
-                      /\ expr.wf G e e).
+          Fixpoint reify_interp_related {t with_lets} v1 v2 {struct t}
+            : @value_interp_related t with_lets v1 v2
+              -> expr_interp_related (reify v1) v2
+          with reflect_interp_related {t with_lets} e1 v2 {struct t}
+               : expr_interp_related e1 v2
+                 -> @value_interp_related t with_lets (reflect e1) v2.
           Proof using Type.
-            split; revert t e H; induction r.
-            all: unshelve
-                   (repeat
-                      first [ progress cbn [rawexpr_interp_ok rawexpr_equiv_expr List.In eq_rect] in *
-                            | progress subst
-                            | progress destruct_head'_and
-                            | progress destruct_head' iff
-                            | progress destruct_head'_ex
-                            | progress destruct_head'_sig
-                            | progress destruct_head'_False
-                            | progress specialize_by_assumption
-                            | progress inversion_sigma
-                            | progress eliminate_hprop_eq
-                            | reflexivity
-                            | progress intros
-                            | break_innermost_match_step
-                            | break_innermost_match_hyps_step
-                            | progress expr.invert_match
-                            | progress expr.inversion_wf_constr
-                            | rewrite in_app_iff in *
-                            | (exists eq_refl)
-                            | apply conj
-                            | match goal with
-                              | [ |- expr.wf _ _ _ ] => constructor
-                              | [ H : forall t e, rawexpr_equiv_expr e ?r -> _, H' : rawexpr_equiv_expr _ ?r |- _ ]
-                                => specialize (H _ _ H')
-                              | [ H : (exists G, _ /\ expr.wf G ?e1 ?e2) -> _, H' : expr.wf ?G' ?e1 ?e2 |- _ ]
-                                => specialize (fun pf1 => H (ex_intro _ G' (conj pf1 H')))
-                              | [ G1 : list ?T, G2 : list ?T |- @ex (list ?T) _ ] => exists (G1 ++ G2)%list
-                              | [ G : list ?T |- @ex (list ?T) _ ] => exists G
-                              | [ |- @ex (list ?T) _ ] => exists (@nil T)
-                              | [ H : ?T, H' : ?T |- _ ] => clear H'
-                              | [ |- ex _ ] => eexists
-                              end
-                            | solve [ eauto ]
-                            | progress destruct_head'_or
-                            | solve [ wf_unsafe_t; wf_safe_t ]
-                            | unshelve erewrite eq_expr_of_rawexpr_equiv_expr; [ .. | eassumption | ]; []
-                            | match goal with
-                              | [ H : ?x = ?y |- _ ] => progress unify x y
-                              | [ |- context[rew ?pf in _] ] => tryif is_var pf then destruct pf else generalize pf
-                              end ]).
-            repeat first [ progress subst
-                         | congruence
-                         | match goal with
-                           | [ H : rawexpr_equiv_expr _ _ |- _ = _ :> type ] => apply eq_type_of_rawexpr_equiv_expr in H
-                           end ].
+            all: destruct t as [|s d];
+              [ clear reify_interp_related reflect_interp_related
+              | pose proof (reify_interp_related s false) as reify_interp_related_s;
+                pose proof (reflect_interp_related s false) as reflect_interp_related_s;
+                pose proof (reify_interp_related d true) as reify_interp_related_d;
+                pose proof (reflect_interp_related d true) as reflect_interp_related_d;
+                clear reify_interp_related reflect_interp_related ].
+            all: repeat first [ progress cbn [reify reflect] in *
+                              | progress fold (@reify) (@reflect) in *
+                              | progress cbn [expr_interp_related value_interp_related] in *
+                              | break_innermost_match_step
+                              | rewrite <- UnderLets.to_expr_interp_related_iff
+                              | exact id
+                              | assumption
+                              | solve [ eauto ]
+                              | progress intros
+                              | match goal with H : _ |- _ => apply H; clear H end
+                              | progress repeat esplit ].
           Qed.
 
-          Lemma rawexpr_equiv_ok_iff {r1 r2} (H : rawexpr_equiv r1 r2)
-            : rawexpr_interp_ok r1 <-> rawexpr_interp_ok r2.
+          Lemma expr_of_rawexpr_interp_related r v
+            : rawexpr_interp_related r v
+              -> expr_interp_related (expr_of_rawexpr r) v.
           Proof using Type.
-            split; revert r1 r2 H; induction r1.
-            all: repeat first [ progress cbn [rawexpr_interp_ok rawexpr_equiv eq_rect projT1 projT2] in *
+            revert v; induction r; cbn [expr_of_rawexpr expr_interp_related rawexpr_interp_related]; intros.
+            all: repeat first [ progress destruct_head'_and
+                              | progress destruct_head'_ex
                               | progress subst
                               | progress inversion_sigma
-                              | progress destruct_head'_ex
-                              | progress destruct_head'_and
-                              | progress destruct_head' iff
-                              | progress destruct_head'_sig
-                              | progress destruct_head'_False
-                              | progress eliminate_hprop_eq
-                              | progress specialize_by_assumption
-                              | reflexivity
-                              | eassumption
-                              | progress intros
-                              | break_innermost_match_hyps_step
-                              | erewrite <- rawexpr_equiv_expr_ok_iff by eassumption
+                              | progress cbn [eq_rect type_of_rawexpr expr.interp expr_interp_related type_of_rawexpr] in *
+                              | assumption
+                              | exfalso; assumption
                               | apply conj
-                              | (exists eq_refl)
+                              | break_innermost_match_hyps_step
                               | solve [ eauto ]
-                              | match goal with
-                                | [ H : rawexpr_equiv_expr _ _ |- _ ] => apply rawexpr_equiv_expr_ok_iff in H
-                                | [ H : (exists G, _ /\ expr.wf G ?e1 ?e2) -> _, H' : expr.wf ?G' ?e1 ?e2 |- _ ]
-                                  => specialize (fun pf1 => H (ex_intro _ G' (conj pf1 H')))
-                                | [ H : type.arrow _ _ = type.arrow _ _ |- _ ] => progress type.inversion_type
-                                | [ H : rawexpr_equiv _ _ |- _ ==== _ ]
-                                  => generalize (eq_type_of_rawexpr_equiv H) (eq_expr_of_rawexpr_equiv H); clear H
-                                | [ |- context[rew ?pf in _] ] => is_evar pf; generalize pf
-                                end ].
-            all: match goal with |- exists s d pff pfx, _ ==== _ => idtac end.
-            all: repeat first [ progress intros
-                              | progress subst
-                              | progress cbn [eq_rect] in *
-                              | (exists eq_refl)
-                              | reflexivity
-                              | match goal with
-                                | [ H : rawexpr_equiv ?r1 ?r2 |- _ ]
-                                  => generalize (eq_type_of_rawexpr_equiv H) (eq_expr_of_rawexpr_equiv H); clear H
-                                | [ |- context[expr_of_rawexpr ?r] ] => generalize dependent (expr_of_rawexpr r)
-                                | [ H : type_of_rawexpr ?r = _ |- _ ] => generalize dependent (type_of_rawexpr r)
-                                | [ H : _ = type_of_rawexpr ?r |- _ ] => generalize dependent (type_of_rawexpr r)
-                                | [ |- ex _ ] => eexists
-                                end ].
+                              | apply reify_interp_related ].
           Qed.
 
-          Lemma reveal_rawexpr_ok_iff {r}
-            : rawexpr_interp_ok (reveal_rawexpr r) <-> rawexpr_interp_ok r.
-          Proof using Type. apply rawexpr_equiv_ok_iff, reveal_rawexpr_equiv. Qed.
-
-          Fixpoint pattern_default_interp' {K t} (p : pattern t) evm {struct p} : (expr (pattern.type.subst_default t evm) -> K) -> @with_unification_resultT' t p evm K
-            := match p in pattern.pattern t return (expr (pattern.type.subst_default t evm) -> K) -> @with_unification_resultT' t p evm K with
-               | pattern.Wildcard t => fun k v => k (reify v)
+          Fixpoint pattern_default_interp' {K t} (p : pattern t) evm {struct p} : (var (pattern.type.subst_default t evm) -> K) -> @with_unification_resultT' var t p evm K
+            := match p in pattern.pattern t return (var (pattern.type.subst_default t evm) -> K) -> @with_unification_resultT' var t p evm K with
+               | pattern.Wildcard t => fun k v => k v
                | pattern.Ident t idc
                  => fun k
-                    => lam_type_of_list (fun args => k (expr.Ident (pident_to_typed _ idc _ args)))
+                    => lam_type_of_list (fun args => k (ident_interp _(pident_to_typed _ idc _ args)))
                | pattern.App s d f x
                  => fun k
                     => @pattern_default_interp'
@@ -2425,10 +2063,12 @@ Module Compilers.
                           => @pattern_default_interp'
                                _ _ x evm
                                (fun ex
-                                => k (expr.App ef ex)))
+                                => k (ef ex)))
                end.
 
-          Definition pattern_default_interp {t} (p : pattern t) : @with_unif_rewrite_ruleTP_gen t p false false false
+          Definition pattern_default_interp {t} (p : pattern t)
+            : @with_unification_resultT var t p var
+            (*: @with_unif_rewrite_ruleTP_gen var t p false false false*)
             := pattern.type.lam_forall_vars
                  (fun evm
                   => pattern_default_interp' p evm id).
@@ -2436,27 +2076,28 @@ Module Compilers.
           Definition deep_rewrite_ruleTP_gen_good_relation
                      {should_do_again with_opt under_lets : bool} {t}
                      (v1 : @deep_rewrite_ruleTP_gen should_do_again with_opt under_lets t)
-                     (v2 : expr t)
+                     (v2 : var t)
             : Prop
-            := (let v1 := normalize_deep_rewrite_rule v1 in
-                match v1 with
-                | None => True
-                | Some v1 => let v1 := UnderLets.interp ident_interp v1 in
-                             (if should_do_again
-                                 return (@expr.expr base.type ident (if should_do_again then @value var else var) t) -> Prop
-                              then
-                                (fun v1
-                                 => expr.interp ident_interp (reify_expr v1) == expr.interp ident_interp v2)
-                              else
-                                (fun v1 => expr.interp ident_interp v1 == expr.interp ident_interp v2))
-                               v1
-                end).
+            := let v1 := normalize_deep_rewrite_rule v1 in
+               match v1 with
+               | None => True
+               | Some v1 => UnderLets.interp_related
+                              ident_interp
+                              (fun e
+                               => expr_interp_related
+                                    ((if should_do_again
+                                         return (@expr.expr base.type ident (if should_do_again then @value var else var) t) -> _
+                                      then reify_expr
+                                      else fun v1 => v1) e))
+                              v1
+                              v2
+               end.
 
           Definition rewrite_rule_data_interp_goodT
                      {t} {p : pattern t} (r : @rewrite_rule_data t p)
             : Prop
             := forall x y,
-              related_unification_resultT (fun t v1 v2 => value_interp_ok v1 /\ value_interp_ok v2 /\ value'_interp v1 == value'_interp v2) x y
+              related_unification_resultT (fun t => value_interp_related) x y
               -> option_eq
                    (fun fx gy
                     => related_sigT_by_eq
@@ -2464,8 +2105,8 @@ Module Compilers.
                           => @deep_rewrite_ruleTP_gen_good_relation
                                (rew_should_do_again _ _ r) (rew_with_opt _ _ r) (rew_under_lets _ _ r) (pattern.type.subst_default t evm))
                          fx gy)
-                   (app_with_unification_resultT_cps _ (rew_replacement _ _ r) x _ (@Some _))
-                   (app_with_unification_resultT_cps _ (pattern_default_interp p) y _ (@Some _)).
+                   (app_with_unification_resultT_cps (rew_replacement _ _ r) x _ (@Some _))
+                   (app_with_unification_resultT_cps (pattern_default_interp p) y _ (@Some _)).
 
           Definition rewrite_rules_interp_goodT
                      (rews : rewrite_rulesT)
@@ -2497,17 +2138,13 @@ Module Compilers.
             intro H.
             repeat (let x := fresh "x" in intro x; specialize (H x)).
             intros X Y HXY.
-            pose proof (related_app_with_unification_resultT _ _ _ _ _ _ ltac:(eassumption) ltac:(eapply map_related_unification_resultT; [ | eassumption ]; intros; cbv beta in *; destruct_head'_and; eapply value_interp_related_iff_of_ok; eassumption)) as H'.
-            cps_id'_with_option app_with_unification_resultT_cps_id.
-            cbv [deep_rewrite_ruleTP_gen] in *.
-            let H1 := fresh in
-            let H2 := fresh in
-            lazymatch type of H' with
-            | option_eq ?R ?x ?y
-              => destruct x eqn:H1, y eqn:H2; cbv [option_eq] in H'
+            pose proof (related_app_with_unification_resultT _ _ _ _ _ _ ltac:(eassumption) HXY) as H'.
+            progress cbv [deep_rewrite_ruleTP_gen] in *.
+            match goal with
+            | [ H : option_eq ?R ?x ?y |- option_eq ?R' ?x' ?y' ]
+              => change (option_eq R' x y); destruct x eqn:?, y eqn:?; cbv [option_eq] in H |- *
             end.
-            all: repeat first [ progress cbn [option_eq]
-                              | reflexivity
+            all: repeat first [ reflexivity
                               | progress inversion_option
                               | exfalso; assumption
                               | assumption ].
diff --git a/src/Experiments/NewPipeline/RewriterWf2.v b/src/Experiments/NewPipeline/RewriterWf2.v
index 9f4f65a70..42720bd38 100644
--- a/src/Experiments/NewPipeline/RewriterWf2.v
+++ b/src/Experiments/NewPipeline/RewriterWf2.v
@@ -139,8 +139,8 @@ Module Compilers.
           Local Notation wf_with_unification_resultT := (@wf_with_unification_resultT ident pident pident_arg_types type_vars_of_pident var1 var2).
           Local Notation wf_with_unif_rewrite_ruleTP_gen := (@wf_with_unif_rewrite_ruleTP_gen ident pident pident_arg_types type_vars_of_pident var1 var2).
           Local Notation wf_deep_rewrite_ruleTP_gen := (@wf_deep_rewrite_ruleTP_gen ident var1 var2).
-          Local Notation app_with_unification_resultT_cps1 := (@app_with_unification_resultT_cps ident var1 pident pident_arg_types type_vars_of_pident).
-          Local Notation app_with_unification_resultT_cps2 := (@app_with_unification_resultT_cps ident var2 pident pident_arg_types type_vars_of_pident).
+          Local Notation app_with_unification_resultT_cps1 := (@app_with_unification_resultT_cps pident pident_arg_types type_vars_of_pident (@value var1)).
+          Local Notation app_with_unification_resultT_cps2 := (@app_with_unification_resultT_cps pident pident_arg_types type_vars_of_pident (@value var2)).
           Local Notation wf_app_with_unification_resultT := (@wf_app_with_unification_resultT ident pident pident_arg_types type_vars_of_pident var1 var2).
 
           (* Because [proj1] and [proj2] in the stdlib are opaque *)
diff --git a/src/Experiments/NewPipeline/UnderLetsProofs.v b/src/Experiments/NewPipeline/UnderLetsProofs.v
index 101d7e9dd..e6aedd009 100644
--- a/src/Experiments/NewPipeline/UnderLetsProofs.v
+++ b/src/Experiments/NewPipeline/UnderLetsProofs.v
@@ -333,6 +333,18 @@ Module Compilers.
                                  @interp _ (f xv)
              end.
 
+        Fixpoint interp_related {T1 T2} (R : T1 -> T2 -> Prop) (e : UnderLets T1) (v2 : T2) : Prop
+          := match e with
+             | Base v1 => R v1 v2
+             | UnderLet t e f (* combine the App rule with the Abs rule *)
+               => exists fv ev,
+                  expr.interp_related ident_interp e ev
+                  /\ (forall x1 x2,
+                         x1 == x2
+                         -> @interp_related T1 T2 R (f x1) (fv x2))
+                  /\ fv ev = v2
+             end.
+
         Lemma interp_splice {A B} (x : UnderLets A) (e : A -> UnderLets B)
           : interp (splice x e) = interp (e (interp x)).
         Proof. induction x; cbn [splice interp]; eauto. Qed.
@@ -352,6 +364,201 @@ Module Compilers.
         Lemma interp_of_expr {t} (x : expr t)
           : expr.interp ident_interp (interp (of_expr x)) = expr.interp ident_interp x.
         Proof. induction x; cbn [expr.interp interp of_expr]; cbv [LetIn.Let_In]; eauto. Qed.
+
+        Lemma to_expr_interp_related_iff {t e v}
+          : interp_related (expr.interp_related ident_interp (t:=t)) e v
+            <-> expr.interp_related ident_interp (UnderLets.to_expr e) v.
+        Proof using Type.
+          revert v; induction e; cbn [UnderLets.to_expr interp_related expr.interp_related]; try reflexivity.
+          setoid_rewrite H.
+          reflexivity.
+        Qed.
+
+        Global Instance interp_related_Proper_iff {T1 T2}
+          : Proper (pointwise_relation _ (pointwise_relation _ iff) ==> eq ==> eq ==> iff) (@interp_related T1 T2) | 10.
+        Proof using Type.
+          cbv [pointwise_relation respectful Proper].
+          intros R1 R2 HR x y ? x' y' H'; subst y y'.
+          revert x'; induction x; [ apply HR | ]; cbn [interp_related].
+          setoid_rewrite H; reflexivity.
+        Qed.
+
+        Lemma splice_interp_related_iff {A B T R x e} {v : T}
+          : interp_related R (@UnderLets.splice _ ident _ A B x e) v
+            <-> interp_related
+                  (fun xv => interp_related R (e xv))
+                  x v.
+        Proof using Type.
+          revert v; induction x; cbn [UnderLets.splice interp_related]; [ reflexivity | ].
+          match goal with H : _ |- _ => setoid_rewrite H end.
+          reflexivity.
+        Qed.
+
+        Lemma splice_list_interp_related_iff_gen {A B T R x e1 e2 base} {v : T}
+              (He1e2 : forall ls', e1 ls' = e2 (base ++ ls'))
+          : interp_related R (@UnderLets.splice_list _ ident _ A B x e1) v
+            <-> list_rect
+                  (fun _ => list _ -> _ -> Prop)
+                  (fun ls v => interp_related R (e2 ls) v)
+                  (fun x xs recP ls v
+                   => interp_related
+                        (fun x' v => recP (ls ++ [x']) v)
+                        x
+                        v)
+                  x
+                  base
+                  v.
+        Proof using Type.
+          revert base v e1 e2 He1e2; induction x as [|? ? IHx]; cbn [UnderLets.splice_list interp_related list_rect]; intros.
+          { intros; rewrite He1e2, ?app_nil_r; reflexivity. }
+          { setoid_rewrite splice_interp_related_iff.
+            apply interp_related_Proper_iff; [ | reflexivity.. ]; cbv [pointwise_relation]; intros.
+            specialize (fun v => IHx (base ++ [v])).
+            setoid_rewrite IHx; [ reflexivity | ].
+            intros; rewrite He1e2, <- ?app_assoc; reflexivity. }
+        Qed.
+
+        Lemma splice_list_interp_related_iff {A B T R x e} {v : T}
+          : interp_related R (@UnderLets.splice_list _ ident _ A B x e) v
+            <-> list_rect
+                  (fun _ => list _ -> _ -> Prop)
+                  (fun ls v => interp_related R (e ls) v)
+                  (fun x xs recP ls v
+                   => interp_related
+                        (fun x' v => recP (ls ++ [x']) v)
+                        x
+                        v)
+                  x
+                  nil
+                  v.
+        Proof using Type.
+          apply splice_list_interp_related_iff_gen; reflexivity.
+        Qed.
+
+        Lemma splice_interp_related_of_ex {A B T T' RA RB x e} {v : T}
+          : (exists ev (xv : T'),
+                interp_related RA x xv
+                /\ (forall x1 x2,
+                       RA x1 x2
+                       -> interp_related RB (e x1) (ev x2))
+                /\ ev xv = v)
+            -> interp_related RB (@UnderLets.splice _ ident _ A B x e) v.
+        Proof using Type.
+          revert e v; induction x; cbn [interp_related UnderLets.splice]; intros.
+          all: repeat first [ progress destruct_head'_ex
+                            | progress destruct_head'_and
+                            | progress subst
+                            | reflexivity
+                            | match goal with
+                              | [ H : _ |- _ ] => apply H; clear H
+                              end ].
+          do 2 eexists; repeat apply conj; [ eassumption | | ]; intros.
+          { match goal with H : _ |- _ => apply H; clear H end.
+            do 2 eexists; repeat apply conj; now eauto. }
+          { reflexivity. }
+        Qed.
+
+        Lemma splice_list_interp_related_of_ex {A B T T' RA RB x e} {v : T}
+          : (exists ev (xv : list T'),
+                    List.Forall2 (interp_related RA) x xv
+                    /\ (forall x1 x2,
+                           List.length x2 = List.length xv
+                           -> List.Forall2 RA x1 x2
+                           -> interp_related RB (e x1) (ev x2))
+                    /\ ev xv = v)
+            -> interp_related RB (@UnderLets.splice_list _ ident _ A B x e) v.
+        Proof using Type.
+          revert e v; induction x as [|x xs IHxs]; cbn [interp_related UnderLets.splice_list]; intros.
+          all: repeat first [ progress destruct_head'_ex
+                            | progress destruct_head'_and
+                            | progress cbn [List.length] in *
+                            | progress subst
+                            | reflexivity
+                            | match goal with
+                              | [ H : List.Forall2 _ nil ?x |- _ ] => is_var x; inversion H; clear H
+                              | [ H : List.Forall2 _ (cons _ _) ?x |- _ ] => is_var x; inversion H; clear H
+                              | [ |- List.Forall2 _ _ _ ] => constructor
+                              | [ H : _ |- _ ] => apply H; clear H
+                              end ].
+          lazymatch goal with
+          | [ H : forall l1 l2, length l2 = S (length _) -> Forall2 _ l1 l2 -> _ |- _ ]
+            => specialize (fun l ls l' ls' (pf0 : length _ = _) pf1 pf2 => H (cons l ls) (cons l' ls') (f_equal S pf0) (Forall2_cons _ _ pf1 pf2))
+          end.
+          eapply splice_interp_related_of_ex; do 2 eexists; repeat apply conj;
+            intros; [ eassumption | | ].
+          { eapply IHxs.
+            do 2 eexists; repeat apply conj; intros;
+              [ eassumption | | ].
+            { match goal with H : _ |- _ => eapply H; clear H end; eassumption. }
+            { reflexivity. } }
+          { reflexivity. }
+        Qed.
+
+        Lemma list_rect_interp_related {A B Pnil Pcons ls B' Pnil' Pcons' ls' R}
+              (Hnil : interp_related R Pnil Pnil')
+              (Hcons : forall x x',
+                  expr.interp_related ident_interp x x'
+                  -> forall l l',
+                    List.Forall2 (expr.interp_related ident_interp) l l'
+                    -> forall rec rec',
+                      interp_related R rec rec'
+                      -> interp_related R (Pcons x l rec) (Pcons' x' l' rec'))
+              (Hls : List.Forall2 (expr.interp_related ident_interp (t:=A)) ls ls')
+          : interp_related
+              R
+              (list_rect
+                 (fun _ : list _ => UnderLets B)
+                 Pnil
+                 Pcons
+                 ls)
+              (list_rect
+                 (fun _ : list _ => B')
+                 Pnil'
+                 Pcons'
+                 ls').
+        Proof using Type. induction Hls; cbn [list_rect] in *; auto. Qed.
+
+        Lemma nat_rect_interp_related {A PO PS n A' PO' PS' n' R}
+              (Hnil : interp_related R PO PO')
+              (Hcons : forall n rec rec',
+                  interp_related R rec rec'
+                  -> interp_related R (PS n rec) (PS' n rec'))
+              (Hn : n = n')
+          : interp_related
+              R
+              (nat_rect (fun _ => UnderLets A) PO PS n)
+              (nat_rect (fun _ => A') PO' PS' n').
+        Proof using Type. subst n'; induction n; cbn [nat_rect] in *; auto. Qed.
+
+        Lemma nat_rect_arrow_interp_related {A B PO PS n x A' B' PO' PS' n' x' R}
+              {R' : A -> A' -> Prop}
+              (Hnil : forall x x', R' x x' -> interp_related R (PO x) (PO' x'))
+              (Hcons : forall n rec rec',
+                  (forall x x', R' x x' -> interp_related R (rec x) (rec' x'))
+                  -> forall x x',
+                    R' x x'
+                    -> interp_related R (PS n rec x) (PS' n rec' x'))
+              (Hn : n = n')
+              (Hx : R' x x')
+          : interp_related
+              R
+              (nat_rect (fun _ => A -> UnderLets B) PO PS n x)
+              (nat_rect (fun _ => A' -> B') PO' PS' n' x').
+        Proof using Type. subst n'; revert x x' Hx; induction n; cbn [nat_rect] in *; auto. Qed.
+
+        Lemma interp_related_Proper_impl_same_UnderLets {A B B' R1 R2 e v f}
+              (HR : forall e v, (R1 e v : Prop) -> (R2 e (f v) : Prop))
+          : @interp_related A B R1 e v
+            -> @interp_related A B' R2 e (f v).
+        Proof using Type.
+          revert f v HR; induction e; cbn [interp_related]; [ now eauto | ]; intros F v HR H'.
+          destruct H' as [fv H']; exists (fun ev => F (fv ev)).
+          repeat first [ let x := fresh "x" in destruct H' as [x H']; exists x
+                       | let x := fresh "x" in intro x; specialize (H' x)
+                       | let H := fresh "H" in destruct H' as [H H']; split; [ exact H || now subst | ]
+                       | let H := fresh "H" in destruct H' as [H' H]; split; [ | exact H || now subst ] ].
+          auto.
+        Qed.
       End for_interp.
 
       Section for_interp2.