Start setting up abs-int interp proofs

4 files changed, 909 insertions, 866 deletions

diff --git a/_CoqProject b/_CoqProject
index afb75162c..84e328de7 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -244,6 +244,7 @@ src/Experiments/PartialEvaluationWithLetIn.v
 src/Experiments/SimplyTypedArithmetic.v
 src/Experiments/NewPipeline/AbstractInterpretation.v
 src/Experiments/NewPipeline/AbstractInterpretationProofs.v
+src/Experiments/NewPipeline/AbstractInterpretationWf.v
 src/Experiments/NewPipeline/Arithmetic.v
 src/Experiments/NewPipeline/CLI.v
 src/Experiments/NewPipeline/CStringification.v
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
index 8a5905d92..1b985bda2 100644
--- a/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
+++ b/src/Experiments/NewPipeline/AbstractInterpretationProofs.v
@@ -23,6 +23,7 @@ Require Import Crypto.Experiments.NewPipeline.LanguageInversion.
 Require Import Crypto.Experiments.NewPipeline.LanguageWf.
 Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs.
 Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation.
+Require Import Crypto.Experiments.NewPipeline.AbstractInterpretationWf.
 
 Module Compilers.
   Import Language.Compilers.
@@ -31,6 +32,8 @@ Module Compilers.
   Import LanguageInversion.Compilers.
   Import LanguageWf.Compilers.
   Import UnderLetsProofs.Compilers.
+  Import AbstractInterpretationWf.Compilers.
+  Import AbstractInterpretationWf.Compilers.partial.
   Import invert_expr.
 
   Module Import partial.
@@ -54,362 +57,31 @@ Module Compilers.
       Local Notation abstract_domain := (@abstract_domain base_type abstract_domain').
       Local Notation bottom := (@bottom base_type abstract_domain' (@bottom')).
       Local Notation bottom_for_each_lhs_of_arrow := (@bottom_for_each_lhs_of_arrow base_type abstract_domain' (@bottom')).
-
-      Section with_var2.
-        Context {var1 var2 : type -> Type}.
-        Local Notation UnderLets1 := (@UnderLets.UnderLets base_type ident var1).
-        Local Notation UnderLets2 := (@UnderLets.UnderLets base_type ident var2).
-        Local Notation expr1 := (@expr.expr base_type ident var1).
-        Local Notation expr2 := (@expr.expr base_type ident var2).
-        Local Notation value1 := (@value base_type ident var1 abstract_domain').
-        Local Notation value2 := (@value base_type ident var2 abstract_domain').
-        Local Notation value_with_lets1 := (@value_with_lets base_type ident var1 abstract_domain').
-        Local Notation value_with_lets2 := (@value_with_lets base_type ident var2 abstract_domain').
-        Local Notation state_of_value1 := (@state_of_value base_type ident var1 abstract_domain').
-        Local Notation state_of_value2 := (@state_of_value base_type ident var2 abstract_domain').
-        Context (annotate1 : forall (is_let_bound : bool) t, abstract_domain' t -> @expr1 t -> UnderLets1 (@expr1 t))
-                (annotate2 : forall (is_let_bound : bool) t, abstract_domain' t -> @expr2 t -> UnderLets2 (@expr2 t))
-                (annotate_Proper
-                 : forall is_let_bound t G
-                     v1 v2 (Hv : abstract_domain'_R t v1 v2)
-                     e1 e2 (He : expr.wf G e1 e2),
-                    UnderLets.wf (fun G' => expr.wf G') G (annotate1 is_let_bound t v1 e1) (annotate2 is_let_bound t v2 e2))
-                (interp_ident1 : forall t, ident t -> value_with_lets1 t)
-                (interp_ident2 : forall t, ident t -> value_with_lets2 t).
-        Local Notation reify1 := (@reify base_type ident var1 abstract_domain' annotate1 bottom').
-        Local Notation reify2 := (@reify base_type ident var2 abstract_domain' annotate2 bottom').
-        Local Notation reflect1 := (@reflect base_type ident var1 abstract_domain' annotate1 bottom').
-        Local Notation reflect2 := (@reflect base_type ident var2 abstract_domain' annotate2 bottom').
-        Local Notation interp1 := (@interp base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1).
-        Local Notation interp2 := (@interp base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2).
-        Local Notation eval_with_bound'1 := (@eval_with_bound' base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1).
-        Local Notation eval_with_bound'2 := (@eval_with_bound' base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2).
-        Local Notation eval'1 := (@eval' base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1).
-        Local Notation eval'2 := (@eval' base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2).
-        Local Notation eta_expand_with_bound'1 := (@eta_expand_with_bound' base_type ident var1 abstract_domain' annotate1 bottom').
-        Local Notation eta_expand_with_bound'2 := (@eta_expand_with_bound' base_type ident var2 abstract_domain' annotate2 bottom').
-
-        Definition abstract_domain_R {t} : relation (abstract_domain t)
-          := type.related abstract_domain'_R.
-
-        (** This one is tricky.  Because we need to be stable under
-            weakening and reordering of the context, we permit any
-            context for well-formedness of the input in the arrow
-            case, and simply tack on that context at the beginning of
-            the output.  This is sort-of wasteful on the output
-            context, but it's sufficient to prove
-            [wf_value_Proper_list] below, which is what we really
-            need. *)
-        Fixpoint wf_value G {t} : value1 t -> value2 t -> Prop
-          := match t return value1 t -> value2 t -> Prop with
-             | type.base t
-               => fun v1 v2
-                 => abstract_domain_R (fst v1) (fst v2)
-                   /\ expr.wf G (snd v1) (snd v2)
-             | type.arrow s d
-               => fun v1 v2
-                 => abstract_domain_R (fst v1) (fst v2)
-                   /\ (forall seg G' sv1 sv2,
-                         G' = (seg ++ G)%list
-                         -> @wf_value seg s sv1 sv2
-                         -> UnderLets.wf
-                             (fun G' => @wf_value G' d) G'
-                             (snd v1 sv1) (snd v2 sv2))
-             end.
-
-        Definition wf_value_with_lets G {t} : value_with_lets1 t -> value_with_lets2 t -> Prop
-          := UnderLets.wf (fun G' => wf_value G') G.
-
-        Context (interp_ident_Proper
-                 : forall G t idc1 idc2 (Hidc : idc1 = idc2),
-                    wf_value_with_lets G (interp_ident1 t idc1) (interp_ident2 t idc2)).
-
-        Global Instance bottom_Proper {t} : Proper abstract_domain_R (@bottom t) | 10.
-        Proof using bottom'_Proper.
-          clear -bottom'_Proper type_base.
-          cbv [Proper] in *; induction t; cbn; cbv [respectful]; eauto.
-        Qed.
-
-        Global Instance bottom_for_each_lhs_of_arrow_Proper {t}
-          : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) (@bottom_for_each_lhs_of_arrow t) | 10.
-        Proof using bottom'_Proper.
-          clear -bottom'_Proper type_base.
-          pose proof (@bottom_Proper).
-          cbv [Proper] in *; induction t; cbn; cbv [respectful]; eauto.
+      Local Notation abstract_domain_R := (@abstract_domain_R base_type abstract_domain' abstract_domain'_R).
+
+      Section extract.
+        Context (ident_extract : forall t, ident t -> abstract_domain t)
+                {ident_extract_Proper : forall {t}, Proper (eq ==> abstract_domain_R) (ident_extract t)}.
+
+        Local Notation extract' := (@extract' base_type ident abstract_domain' ident_extract).
+        Local Notation extract_gen := (@extract_gen base_type ident abstract_domain' ident_extract).
+
+        Lemma extract'_Proper G
+              (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> @abstract_domain_R t v1 v2)
+              {t}
+          : Proper (expr.wf G ==> abstract_domain_R) (@extract' t).
+        Proof using ident_extract_Proper. apply expr.wf_interp_Proper_gen1, HG. Qed.
+
+        Lemma extract_gen_Proper G
+              (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> @abstract_domain_R t v1 v2)
+              {t}
+          : Proper (expr.wf G ==> type.and_for_each_lhs_of_arrow (@abstract_domain_R) ==> abstract_domain'_R (type.final_codomain t)) (@extract_gen t).
+        Proof using ident_extract_Proper.
+          intros ?? Hwf; cbv [extract_gen respectful abstract_domain_R].
+          rewrite <- type.related_iff_app_curried.
+          eapply extract'_Proper; eassumption.
         Qed.
-
-        Lemma state_of_value_Proper G {t} v1 v2 (Hv : @wf_value G t v1 v2)
-          : abstract_domain_R (state_of_value1 v1) (state_of_value2 v2).
-        Proof using Type.
-          clear -Hv type_base.
-          destruct t, v1, v2, Hv; cbn in *; cbv [respectful]; eauto.
-        Qed.
-
-        Local Hint Resolve (ex_intro _ nil) (ex_intro _ (cons _ nil)).
-        Local Hint Constructors expr.wf ex.
-        Local Hint Unfold List.In.
-
-        Lemma wf_value_Proper_list G1 G2
-              (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2)
-              t e1 e2
-              (Hwf : @wf_value G1 t e1 e2)
-          : @wf_value G2 t e1 e2.
-        Proof using Type.
-          clear -type_base HG1G2 Hwf.
-          revert dependent G1; revert dependent G2; induction t; intros;
-            repeat first [ progress cbn in *
-                         | progress intros
-                         | solve [ eauto ]
-                         | progress subst
-                         | progress destruct_head'_and
-                         | progress destruct_head'_or
-                         | apply conj
-                         | rewrite List.in_app_iff in *
-                         | match goal with H : _ |- _ => apply H; clear H end
-                         | wf_unsafe_t_step
-                         | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ] ].
-        Qed.
-
-        Fixpoint wf_reify (is_let_bound : bool) G {t}
-          : forall v1 v2 (Hv : @wf_value G t v1 v2)
-              s1 s2 (Hs : type.and_for_each_lhs_of_arrow (@abstract_domain_R) s1 s2),
-            UnderLets.wf (fun G' => expr.wf G') G (@reify1 is_let_bound t v1 s1) (@reify2 is_let_bound t v2 s2)
-        with wf_reflect G {t}
-             : forall e1 e2 (He : expr.wf G e1 e2)
-                 s1 s2 (Hs : abstract_domain_R s1 s2),
-            @wf_value G t (@reflect1 t e1 s1) (@reflect2 t e2 s2).
-        Proof using annotate_Proper bottom'_Proper.
-          all: clear -wf_reflect wf_reify annotate_Proper type_base bottom'_Proper.
-          all: pose proof (@bottom_for_each_lhs_of_arrow_Proper); cbv [Proper] in *.
-          { destruct t as [t|s d];
-              [ clear wf_reify wf_reflect
-              | specialize (fun G => wf_reflect G s);
-                specialize (fun G => wf_reify false G d) ].
-            { cbn; intros [? ?] [? ?] [Hv0 Hv1] [] [] [];
-                cbn [fst snd] in *.
-              apply annotate_Proper; assumption. }
-            { cbn; cbv [respectful]; intros [? ?] [? ?] [He0 He1] [? ?] [? ?] [Hs0 Hs1];
-                cbn [fst snd] in *.
-              do 2 constructor; intros v1 v2.
-              eapply UnderLets.wf_to_expr, UnderLets.wf_splice.
-              { eapply He1 with (seg:=cons _ nil); eauto using eq_refl. }
-              { intros; apply wf_reify; destruct_head'_ex; subst; auto. } } }
-          { destruct t as [t|s d];
-              [ clear wf_reify wf_reflect
-              | specialize (fun G => wf_reflect G d);
-                specialize (fun G => wf_reify false G s) ].
-            { cbn; auto. }
-            { cbn; cbv [respectful]; intros e1 e2 He s1 s2 Hs;
-                split; [ solve [ auto ] | ];
-                  intros G' seg sv1 sv2 HG1G2 Hsv; subst.
-              eapply UnderLets.wf_splice.
-              { apply wf_reify; auto; eapply wf_value_Proper_list; [ .. | solve [ eauto ] ];
-                  wf_safe_t. }
-              { intros G'' a1 a2 [seg' ?] Ha; subst G''.
-                constructor.
-                apply wf_reflect.
-                { constructor; auto; wf_unsafe_t_step; [].
-                  destruct_head'_ex; subst.
-                  intros *.
-                  rewrite !List.in_app_iff; auto. }
-                { eapply Hs, state_of_value_Proper; eassumption. } } } }
-        Qed.
-
-        Local Ltac wf_interp_t :=
-          repeat first [ progress cbv [wf_value_with_lets abstract_domain_R respectful] in *
-                       | progress cbn [wf_value fst snd partial.bottom type.related eq_rect List.In] in *
-                       | wf_safe_t_step
-                       | exact I
-                       | apply wf_reify
-                       | apply bottom_Proper
-                       | progress destruct_head'_ex
-                       | progress destruct_head'_or
-                       | eapply UnderLets.wf_splice
-                       | match goal with
-                         | [ |- UnderLets.wf _ _ _ _ ] => constructor
-                         | [ |- and _ _ ] => apply conj
-                         end
-                       | eapply wf_value_Proper_list; [ | solve [ eauto ] ]
-                       | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ]
-                       | match goal with
-                         | [ H : _ |- _ ] => eapply H; clear H; solve [ wf_interp_t ]
-                         end
-                       | break_innermost_match_step ].
-
-        Lemma wf_interp G G' {t} (e1 : @expr (@value_with_lets1) t) (e2 : @expr (@value_with_lets2) t)
-              (Hwf : expr.wf G e1 e2)
-              (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
-          : wf_value_with_lets G' (interp1 e1) (interp2 e2).
-        Proof using annotate_Proper bottom'_Proper interp_ident_Proper.
-          revert dependent G'; induction Hwf; intros; cbn [interp];
-            try solve [ apply interp_ident_Proper; auto
-                      | eauto ];
-            wf_interp_t.
-        Qed.
-
-        Lemma wf_eval_with_bound' G G' {t} e1 e2 (He : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
-              (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
-          : expr.wf G' (@eval_with_bound'1 t e1 st1) (@eval_with_bound'2 t e2 st2).
-        Proof using annotate_Proper bottom'_Proper interp_ident_Proper.
-          eapply UnderLets.wf_to_expr, UnderLets.wf_splice.
-          { eapply wf_interp; solve [ eauto ]. }
-          { intros; destruct_head'_ex; subst; eapply wf_reify; eauto. }
-        Qed.
-
-        Lemma wf_eval' G G' {t} e1 e2 (He : expr.wf G e1 e2)
-              (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
-          : expr.wf G' (@eval'1 t e1) (@eval'2 t e2).
-        Proof using annotate_Proper bottom'_Proper interp_ident_Proper.
-          eapply wf_eval_with_bound'; eauto; apply bottom_for_each_lhs_of_arrow_Proper.
-        Qed.
-
-        Lemma wf_eta_expand_with_bound' G {t} e1 e2 (He : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
-          : expr.wf G (@eta_expand_with_bound'1 t e1 st1) (@eta_expand_with_bound'2 t e2 st2).
-        Proof using annotate_Proper bottom'_Proper.
-          eapply UnderLets.wf_to_expr, wf_reify; [ eapply wf_reflect | ]; eauto; apply bottom_Proper.
-        Qed.
-
-        (*
-        Lemma related_force {t} x y
-          : @lazy_abstract_domain_R t x y <-> @abstract_domain_R t (force_abstract_domain x) (force_abstract_domain y).
-        Proof.
-          induction t as [t|s IHs d IHd]; [ reflexivity | ].
-          cbv [lazy_abstract_domain_R abstract_domain_R] in *; cbn [type.related] in *; cbv [respectful] in *.
-          setoid_rewrite IHs; setoid_rewrite IHd.
-          progress change (@force_abstract_domain (s -> d)) with (fun f x => @force_abstract_domain d (f (@thunk_abstract_domain s x))).
-          cbv beta iota.
-          (*progress change (@thunk_abstract_domain (s -> d)) with (fun f x => @thunk_abstract_domain d (f (@force_abstract_domain s x))).*)
-          intuition.
-          { match goal with
-            | [ H : _ |- _ ] => apply H; rewrite !force_thunk_abstract_domain_ext; assumption
-            end. }
-          { match goal with
-            | [ |- ?R (force_abstract_domain (?f ?x)) (force_abstract_domain (?g ?y)) ]
-              => rewrite <- (force_thunk_abstract_domain_ext x),  <- (force_thunk_abstract_domain_ext y)
-            end.
-          eauto.
-          intuition (rewrite ?force_thunk_abstract_domain_ext; eauto).
-          apply H.
-         *)
-        (*
-        Section extract.
-          Context (ident_extract : forall t, ident t -> lazy_abstract_domain t)
-                  {ident_extract_Proper : forall {t}, Proper (eq ==> lazy_abstract_domain_R) (ident_extract t)}.
-
-          Local Notation extract' := (@extract' base_type ident abstract_domain' ident_extract).
-          Local Notation extract_gen := (@extract_gen base_type ident abstract_domain' ident_extract).
-
-          Lemma extract'_Proper G
-                (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> @lazy_abstract_domain_R t v1 v2)
-                {t}
-            : Proper (expr.wf G ==> lazy_abstract_domain_R) (@extract' t).
-          Proof using ident_extract_Proper.
-            clear -ident_extract_Proper HG type_base; cbv [lazy_abstract_domain_R].
-            intros ? ? Hwf.
-            induction Hwf; red_thunk_force; cbn -[thunk_abstract_domain force_abstract_domain] in *; red_thunk_force;
-              cbv [respectful] in *; try apply ident_extract_Proper; intros; eauto;
-                try solve [ repeat first [ progress intros
-                             | progress cbn [List.In fst snd] in *
-                           | progress cbv [lazy_abstract_domain_R] in *
-                           | rewrite force_thunk_abstract_domain_ext
-                             | progress wf_safe_t
-                             | match goal with
-                               | [ H : _ |- _ ] => eapply H; clear H
-                               end ] ].
-            repeat first [ progress intros
-                             | progress cbn [List.In fst snd] in *
-                           | progress cbv [lazy_abstract_domain_R] in *
-                           | rewrite force_thunk_abstract_domain_ext
-                           | progress wf_safe_t ].
-            eapply IHHwf1.
-            match goal with
-            | [ H : _ |- _ ] => eapply H; clear H
-            end.
-            { repeat first [ progress intros
-                           | progress cbn [List.In fst snd] in *
-                           | progress cbv [lazy_abstract_domain_R] in *
-                           | rewrite force_thunk_abstract_domain_ext
-                           | progress wf_safe_t ].
-              .
-
-          Qed.
-
-          Local Lemma pull_prod_forall A A' B B' (Q : A * A' -> B * B' -> Prop)
-            : (forall x y, Q x y) <-> (forall x0 y0 x1 y1, Q (x0, x1) (y0, y1)).
-          Proof. intuition. Qed.
-
-          Lemma abstract_domain_R_app_curried_iff t F G
-            : (@abstract_domain_R t F G)
-              <-> (forall x y, type.and_for_each_lhs_of_arrow (@abstract_domain_R) x y -> abstract_domain'_R (type.final_codomain t) (type.app_curried F x) (type.app_curried G y)).
-          Proof using Type.
-            clear -type_base.
-            induction t as [t|s IHs d IHd]; cbn; [ tauto | ].
-            cbv [respectful].
-            rewrite pull_prod_forall.
-            lazymatch goal with
-            | [ |- (forall x y, @?P x y) <-> (forall z w, @?Q z w) ]
-              => cut (forall x y, (P x y <-> Q x y)); [ intro H'; setoid_rewrite H'; reflexivity | intros ??; cbn [fst snd] ]
-            end.
-            lazymatch goal with
-            | [ |- (?P -> ?Q) <-> (forall z w, ?P' /\ @?R z w -> @?S z w) ]
-              => unify P P'; cut (P' -> (Q <-> (forall z w, R z w -> S z w))); [ change P with P'; solve [ intuition ] | intro; cbn [fst snd] ]
-            end.
-            eauto.
-          Qed.
-
-          Lemma lazy_abstract_domain_R_app_curried_iff t F G
-            : (@lazy_abstract_domain_R t F G)
-              <-> (forall x y, type.and_for_each_lhs_of_arrow (@abstract_domain_R) x y -> abstract_domain'_R (type.final_codomain t) (type.app_curried F (type.map_for_each_lhs_of_arrow (@thunk_abstract_domain) x) tt) (type.app_curried G (type.map_for_each_lhs_of_arrow (@thunk_abstract_domain) y) tt)).
-          Proof using Type.
-            clear -type_base.
-            induction t as [t|s IHs d IHd]; cbn; [ tauto | ].
-            cbv [respectful].
-            rewrite pull_prod_forall; cbn.
-            lazymatch goal with
-            | [ |- (forall x y, @?P x y) <-> (forall z w, @?Q z w) ]
-              => cut (forall x y, (P x y <-> Q (force_abstract_domain x) (force_abstract_domain y))); [ intro H'; setoid_rewrite H' | intros ??; cbn [fst snd] ]
-            end.
-            { cbn; intuition.
-              match goal with
-              | [ H : _ |- ?R (type.app_curried (?F ?x) _ _) (type.app_curried (?G ?y) _ _) ]
-                => specialize (H x y); rewrite !force_thunk_abstract_domain_ext in H; apply H; auto
-              end. }
-            lazymatch goal with
-            | [ |- (?P -> ?Q) <-> (forall z w, ?P' /\ @?R z w -> @?S z w) ]
-              => unify P P'; cut (P' -> (Q <-> (forall z w, R z w -> S z w))); [ change P with P'; solve [ intuition ] | intro; cbn [fst snd] ]
-            end.
-            eauto.
-          Qed.
-
-          Lemma extract_gen_Proper G
-                (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> @lazy_abstract_domain_R t v1 v2)
-                {t}
-            : Proper (expr.wf G ==> type.and_for_each_lhs_of_arrow (@abstract_domain_R) ==> abstract_domain'_R (type.final_codomain t)) (@extract_gen t).
-          Proof.
-            intros ?? Hwf ?? Hv; cbv [extract_gen].
-            generalize (@extract'_Proper G HG t _ _ Hwf).
-            generalize (extract' x) (extract' y); clear x y G HG Hwf; intros x y Hwf.
-            generalize (conj Hv Hwf).
-            clear Hv Hwf.
-
-            setoid_rewrite abstract_domain_R_app_curried_iff.
-            lazymatch goal with
-            | [ |- ?X -> ?Y ] => cut (X <-> Y); [ tauto | ]
-            end.
-            induction t; [ solve [ intuition eauto; constructor ] | ];
-              cbn [type.final_codomain type.app_curried type.for_each_lhs_of_arrow type.and_for_each_lhs_of_arrow type.map_for_each_lhs_of_arrow fst snd] in *.
-            destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *.
-            rewrite <- IHt2.
-            rewrite !and_assoc, !(and_comm (type.and_for_each_lhs_of_arrow _ _ _)), <- !and_assoc.
-            lazymatch goal with
-            | [ |- (?A /\ ?B) <-> (?C /\ ?B) ] => cut (A <-> C); [ tauto | ]
-            end.
-          Definition extract_gen {t} (e : @expr lazy_abstract_domain t) (bound : type.for_each_lhs_of_arrow abstract_domain t)
-            : abstract_domain' (type.final_codomain t)
-            := type.app_curried (extract' e) (type.map_for_each_lhs_of_arrow (@thunk_abstract_domain) bound) tt.
-        End extract.*)
-
-      End with_var2.
+      End extract.
     End with_type.
 
     Module ident.
@@ -433,338 +105,17 @@ Module Compilers.
                 (extract_list_state_length : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2))
                 (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2).
 
-        Local Instance abstract_interp_ident_Proper_arrow s d
-          : Proper (eq ==> abstract_domain'_R s ==> abstract_domain'_R d) (abstract_interp_ident (type.arrow s d))
-          := abstract_interp_ident_Proper (type.arrow s d).
-
-        Section with_var2.
-          Context {var1 var2 : type -> Type}.
-
-          Local Notation update_annotation1 := (@ident.update_annotation var1 abstract_domain' annotate_ident abstract_interp_ident is_annotation).
-          Local Notation update_annotation2 := (@ident.update_annotation var2 abstract_domain' annotate_ident abstract_interp_ident is_annotation).
-          Local Notation annotate1 := (@ident.annotate var1 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
-          Local Notation annotate2 := (@ident.annotate var2 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
-          Local Notation annotate_base1 := (@ident.annotate_base var1 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state is_annotation).
-          Local Notation annotate_base2 := (@ident.annotate_base var2 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state is_annotation).
-          Print ident.annotate_with_ident.
-          Local Notation annotate_with_ident1 := (@ident.annotate_with_ident var1 abstract_domain' annotate_ident abstract_interp_ident is_annotation).
-          Local Notation annotate_with_ident2 := (@ident.annotate_with_ident var2 abstract_domain' annotate_ident abstract_interp_ident is_annotation).
-          Local Notation interp_ident1 := (@ident.interp_ident var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
-          Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
-          Local Notation reflect1 := (@reflect base.type ident var1 abstract_domain' annotate1 bottom').
-          Local Notation reflect2 := (@reflect base.type ident var2 abstract_domain' annotate2 bottom').
-
-          Lemma wf_update_annotation G {t} st1 st2 (Hst : abstract_domain'_R t st1 st2) e1 e2 (He : expr.wf G e1 e2)
-            : expr.wf G (@update_annotation1 t st1 e1) (@update_annotation2 t st2 e2).
-          Proof.
-            cbv [ident.update_annotation];
-              repeat first [ progress subst
-                           | progress expr.invert_subst
-                           | progress cbn [fst snd projT1 projT2 eq_rect] in *
-                           | progress cbn [invert_AppIdent Option.bind invert_App invert_Ident] in *
-                           | progress destruct_head'_sig
-                           | progress destruct_head'_sigT
-                           | progress destruct_head'_and
-                           | progress destruct_head'_prod
-                           | progress destruct_head' False
-                           | progress inversion_option
-                           | progress expr.inversion_wf_constr
-                           | progress expr.inversion_wf_one_constr
-                           | break_innermost_match_hyps_step
-                           | expr.invert_match_step
-                           | progress expr.inversion_expr
-                           | progress rewrite_type_transport_correct
-                           | progress type_beq_to_eq
-                           | progress type.inversion_type
-                           | progress base.type.inversion_type
-                           | match goal with
-                             | [ H : abstract_domain'_R _ ?x _ |- _ ] => rewrite !H; clear dependent x
-                             end
-                           | progress wf_safe_t
-                           | break_innermost_match_step ].
-          Qed.
-
-          Lemma wf_annotate_with_ident
-                is_let_bound t G
-                v1 v2 (Hv : abstract_domain'_R t v1 v2)
-                e1 e2 (He : expr.wf G e1 e2)
-            : UnderLets.wf (fun G' => expr.wf G') G (@annotate_with_ident1 is_let_bound t v1 e1) (@annotate_with_ident2 is_let_bound t v2 e2).
-          Proof.
-            cbv [ident.annotate_with_ident]; break_innermost_match; repeat constructor; apply wf_update_annotation; assumption.
-          Qed.
-
-          Lemma wf_annotate_base
-                is_let_bound (t : base.type.base) G
-                v1 v2 (Hv : abstract_domain'_R t v1 v2)
-                e1 e2 (He : expr.wf G e1 e2)
-            : UnderLets.wf (fun G' => expr.wf G') G (@annotate_base1 is_let_bound t v1 e1) (@annotate_base2 is_let_bound t v2 e2).
-          Proof.
-            cbv [ident.annotate_base];
-              repeat first [ apply wf_annotate_with_ident
-                           | break_innermost_match_step
-                           | progress subst
-                           | progress cbv [type_base ident.smart_Literal] in *
-                           | progress cbn [invert_Literal ident.invert_Literal] in *
-                           | discriminate
-                           | progress destruct_head' False
-                           | progress expr.invert_subst
-                           | progress expr.inversion_wf
-                           | wf_safe_t_step
-                           | break_innermost_match_hyps_step
-                           | match goal with
-                             | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H
-                             | [ |- UnderLets.wf _ _ _ _ ] => constructor
-                             | [ H : abstract_domain'_R _ _ _ |- _ ] => rewrite !H
-                             end
-                           | progress expr.invert_match_step
-                           | progress expr.inversion_expr ].
-          Qed.
-
-          Lemma wf_annotate
-                is_let_bound t G
-                v1 v2 (Hv : abstract_domain'_R t v1 v2)
-                e1 e2 (He : expr.wf G e1 e2)
-            : UnderLets.wf (fun G' => expr.wf G') G (@annotate1 is_let_bound t v1 e1) (@annotate2 is_let_bound t v2 e2).
-          Proof.
-            revert dependent G; induction t; intros;
-              cbn [ident.annotate]; try apply wf_annotate_base; trivial.
-            all: repeat first [ lazymatch goal with
-                                | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e1 = Some _, H'' : reflect_list ?e2 = None |- _ ]
-                                  => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence
-                                | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e2 = Some _, H'' : reflect_list ?e1 = None |- _ ]
-                                  => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence
-                                | [ H : expr.wf _ (reify_list _) (reify_list _) |- _ ] => apply expr.wf_reify_list in H
-                                | [ |- expr.wf _ (reify_list _) (reify_list _) ] => apply expr.wf_reify_list
-                                | [ |- UnderLets.wf _ _ (UnderLets.splice_list _ _) (UnderLets.splice_list _ _) ]
-                                  => eapply @UnderLets.wf_splice_list_no_order with (P:=fun G => expr.wf G); autorewrite with distr_length
-                                | [ H : expr.wf _ (reify_list _) ?e, H' : reflect_list ?e = None |- _ ]
-                                  => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence
-                                | [ H : expr.wf _ ?e (reify_list _), H' : reflect_list ?e = None |- _ ]
-                                  => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence
-                                | [ H : extract_list_state ?t ?v1 = ?x1, H' : extract_list_state ?t ?v2 = ?x2, Hv : abstract_domain'_R _ ?v1 ?v2 |- _ ]
-                                  => let Hl := fresh in
-                                     let Hl' := fresh in
-                                     pose proof (extract_list_state_length _ v1 v2 Hv) as Hl;
-                                     pose proof (extract_list_state_rel _ v1 v2 Hv) as Hl';
-                                     rewrite H, H' in Hl, Hl'; cbv [option_eq option_map] in Hl, Hl'; clear H H'
-                                | [ H : ?x = ?x |- _ ] => clear H
-                                | [ H : length ?l1 = length ?l2, H' : context[length ?l1] |- _ ] => rewrite H in H'
-                                end
-                              | apply wf_annotate_with_ident
-                              | apply DefaultValue.expr.base.wf_default
-                              | apply DefaultValue.expr.wf_default
-                              | progress expr.invert_subst
-                              | progress cbn [ident.annotate ident.smart_Literal invert_Literal ident.invert_Literal invert_pair invert_AppIdent2 invert_App2 fst snd projT2 projT1 eq_rect Option.bind] in *
-                              | progress destruct_head' False
-                              | progress inversion_option
-                              | progress destruct_head'_ex
-                              | discriminate
-                              | wf_safe_t_step
-                              | progress expr.inversion_wf_constr
-                              | progress expr.inversion_expr
-                              | progress type_beq_to_eq
-                              | progress type.inversion_type
-                              | progress base.type.inversion_type
-                              | match goal with
-                                | [ |- expr.wf _ (update_annotation1 _ _) (update_annotation2 _ _) ] => apply wf_update_annotation
-                                | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H
-                                | [ |- UnderLets.wf _ _ _ _ ] => constructor
-                                | [ H : abstract_domain'_R _ ?x _ |- _ ] => rewrite !H
-                                | [ |- UnderLets.wf _ _ (UnderLets.splice _ _) (UnderLets.splice _ _) ] => eapply UnderLets.wf_splice
-                                | [ H : List.nth_error (List.map _ _) _ = Some _ |- _ ] => apply nth_error_map in H
-                                | [ H : context[List.nth_error (List.combine _ _) _] |- _ ] => rewrite nth_error_combine in H
-                                | [ |- context[List.nth_error (List.combine _ _) _] ] => rewrite nth_error_combine
-                                | [ H : forall x y, Some _ = Some _ -> Some _ = Some _ -> _ |- _ ]
-                                  => specialize (H _ _ eq_refl eq_refl)
-                                | [ H : forall v1 v2, List.In (v1, v2) (List.combine ?l1 ?l2) -> ?R v1 v2, H' : List.nth_error ?l1 ?n = Some ?a1, H'' : List.nth_error ?l2 ?n = Some ?a2
-                                                                                                                                                  |- ?R ?a1 ?a2 ]
-                                  => apply H
-                                | [ H : List.nth_error ?l ?n' = Some ?v |- List.In (?v, _) (List.combine ?l _) ] => apply nth_error_In with (n:=n')
-                                end
-                              | break_innermost_match_step
-                              | break_innermost_match_hyps_step
-                              | progress expr.invert_match
-                              | progress expr.inversion_wf_one_constr
-                              | match goal with
-                                | [ H : context[UnderLets.wf _ _ (annotate1 _ _ _) (annotate2 _ _ _)]
-                                    |- UnderLets.wf _ _ (annotate1 _ _ _) (annotate2 _ _ _) ] => eapply H
-                                end
-                              | apply abstract_interp_ident_Proper_arrow
-                              | progress rewrite_type_transport_correct
-                              | apply conj
-                              | congruence
-                              | solve [ wf_t ] ].
-          Qed.
-
-          Local Notation wf_value_with_lets := (@wf_value_with_lets base.type ident abstract_domain' abstract_domain'_R var1 var2).
-          Local Notation wf_value := (@wf_value base.type ident abstract_domain' abstract_domain'_R var1 var2).
-
-          Lemma wf_interp_ident_nth_default G T
-            : wf_value_with_lets G (@interp_ident1 _ (@ident.List_nth_default T)) (@interp_ident2 _ (@ident.List_nth_default T)).
-          Proof.
-            cbv [wf_value_with_lets wf_value ident.interp_ident]; constructor; cbn -[abstract_domain_R abstract_domain].
-            split.
-            { exact (abstract_interp_ident_Proper _ (@ident.List_nth_default T) _ eq_refl). }
-            { intros; subst.
-              destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *.
-              repeat first [ progress subst
-                           | progress cbn [invert_Literal ident.invert_Literal] in *
-                           | lazymatch goal with
-                             | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e1 = Some _, H'' : reflect_list ?e2 = None |- _ ]
-                               => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence
-                             | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e2 = Some _, H'' : reflect_list ?e1 = None |- _ ]
-                               => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence
-                             | [ H : expr.wf _ (reify_list _) (reify_list _) |- _ ] => apply expr.wf_reify_list in H
-                             | [ |- expr.wf _ (reify_list _) (reify_list _) ] => apply expr.wf_reify_list
-                             | [ |- UnderLets.wf _ _ (UnderLets.splice_list _ _) (UnderLets.splice_list _ _) ]
-                               => eapply @UnderLets.wf_splice_list_no_order with (P:=fun G => expr.wf G); autorewrite with distr_length
-                             | [ H : expr.wf _ (reify_list _) ?e, H' : reflect_list ?e = None |- _ ]
-                               => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence
-                             | [ H : expr.wf _ ?e (reify_list _), H' : reflect_list ?e = None |- _ ]
-                               => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence
-                             | [ H : extract_list_state ?t ?v1 = ?x1, H' : extract_list_state ?t ?v2 = ?x2, Hv : abstract_domain_R ?v1 ?v2 |- _ ]
-                               => let Hl := fresh in
-                                  let Hl' := fresh in
-                                  pose proof (extract_list_state_length _ v1 v2 Hv) as Hl;
-                                  pose proof (extract_list_state_rel _ v1 v2 Hv) as Hl';
-                                  rewrite H, H' in Hl, Hl'; cbv [option_eq option_map] in Hl, Hl'; clear H H'
-                             | [ H : ?x = ?x |- _ ] => clear H
-                             | [ H : length ?l1 = length ?l2, H' : context[length ?l1] |- _ ] => rewrite H in H'
-                             end
-                           | match goal with
-                             | [ |- UnderLets.wf ?Q ?G (UnderLets.splice ?x1 ?e1) (UnderLets.splice ?x2 ?e2) ]
-                               => simple refine (@UnderLets.wf_splice _ _ _ _ _ _ _ _ _ Q G x1 x2 _ e1 e2 _);
-                                  [ let G := fresh "G" in
-                                    intro G;
-                                    lazymatch goal with
-                                    | [ |- (abstract_domain ?t * _) -> _ -> _ ]
-                                      => refine (@wf_value G t)
-                                    | [ |- expr _ -> _ -> _ ]
-                                      => refine (expr.wf G)
-                                    end
-                                  | | ]
-                             | [ |- UnderLets.wf ?Q ?G (UnderLets.Base _) (UnderLets.Base _) ]
-                               => constructor
-                             | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H
-                             | [ H : List.nth_error _ _ = None |- _ ] => apply List.nth_error_None in H
-                             | [ H : List.nth_error _ _ = Some _ |- _ ]
-                               => unique pose proof (@ListUtil.nth_error_value_length _ _ _ _ H);
-                                  unique pose proof (@ListUtil.nth_error_value_In _ _ _ _ H)
-                             | [ H : context[List.In _ (List.map _ _)] |- _ ] => rewrite List.in_map_iff in H
-                             | [ H : (?x <= ?y)%nat, H' : (?y < ?x)%nat |- _ ] => exfalso; clear -H H'; lia
-                             | [ H : (?x <= ?y)%nat, H' : (?y < ?x')%nat, H'' : ?x' = ?x |- _ ] => exfalso; clear -H H' H''; lia
-                             | [ H : length ?x = length ?y |- context[length ?x] ] => rewrite H
-                             | [ H : List.nth_error (List.map _ _) _ = Some _ |- _ ] => apply nth_error_map in H
-                             | [ H : context[List.nth_error (List.combine _ _) _] |- _ ] => rewrite nth_error_combine in H
-                             | [ |- context[List.nth_error (List.combine _ _) _] ] => rewrite nth_error_combine
-                             | [ H : forall x y, Some _ = Some _ -> Some _ = Some _ -> _ |- _ ]
-                               => specialize (H _ _ eq_refl eq_refl)
-                             | [ H : forall v1 v2, List.In (v1, v2) (List.combine ?l1 ?l2) -> ?R v1 v2, H' : List.nth_error ?l1 ?n' = Some ?a1, H'' : List.nth_error ?l2 ?n' = Some ?a2
-                                                                                                                                                |- _ ]
-                               => unique pose proof (H a1 a2 ltac:(apply nth_error_In with (n:=n'); rewrite nth_error_combine, H', H''; reflexivity))
-                             | [ H : List.nth_error ?l ?n' = Some ?v |- List.In (?v, _) (List.combine ?l _) ] => apply nth_error_In with (n:=n')
-                             | [ H : context[length ?ls] |- _ ] => tryif is_var ls then fail else (progress autorewrite with distr_length in H)
-                             | [ H : context[List.nth_error (List.seq _ _) _] |- _ ] => rewrite nth_error_seq in H
-                             end
-                           | progress inversion_option
-                           | progress intros
-                           | progress cbn [fst snd value] in *
-                           | progress destruct_head'_prod
-                           | progress destruct_head'_ex
-                           | progress destruct_head'_and
-                           | progress destruct_head' False
-                           | progress specialize_by_assumption
-                           | apply conj
-                           | progress expr.invert_subst
-                           | progress expr.inversion_wf_constr
-                           | progress expr.inversion_expr
-                           | wf_safe_t_step
-                           | progress destruct_head' (@partial.wf_value)
-                           | solve [ eapply wf_annotate; wf_t; try apply DefaultValue.expr.base.wf_default
-                                   | eapply wf_annotate_base; wf_t
-                                   | eapply (abstract_interp_ident_Proper _ (@ident.List_nth_default T) _ eq_refl); assumption
-                                   | eapply wf_update_annotation; wf_t
-                                   | wf_t
-                                   | match goal with
-                                     | [ H : context[UnderLets.wf _ _ _ _] |- UnderLets.wf _ _ _ _ ] => eapply H; solve [ repeat esplit; eauto ]
-                                     end
-                                   | eauto using List.nth_error_In
-                                   | eapply expr.wf_Proper_list; [ | eassumption ]; wf_safe_t; eauto 10 ]
-                           | break_innermost_match_step
-                           | match goal with
-                             | [ H : context[List.In] |- expr.wf _ ?x ?y ]
-                               => specialize (H x y); rewrite !List.nth_default_eq, <- List.combine_nth, <- !List.nth_default_eq in H; cbv [List.nth_default] in H |- *
-                             | [ H : List.In _ _ -> ?P |- ?P ] => apply H
-                             end
-                           | break_innermost_match_hyps_step
-                           | congruence
-                           | rewrite List.combine_length in *
-                           | rewrite NPeano.Nat.min_r in * by lia
-                           | rewrite NPeano.Nat.min_l in * by lia
-                           | progress expr.inversion_wf_one_constr
-                           | progress expr.invert_match ]. }
-          Qed.
-
-          Lemma wf_interp_ident_not_nth_default G {t} (idc : ident t)
-            : wf_value_with_lets G (Base (reflect1 (###idc)%expr (abstract_interp_ident _ idc))) (Base (reflect2 (###idc)%expr (abstract_interp_ident _ idc))).
-          Proof.
-            constructor; eapply wf_reflect;
-              solve [ apply bottom'_Proper
-                    | apply wf_annotate
-                    | repeat constructor
-                    | apply abstract_interp_ident_Proper; reflexivity ].
-          Qed.
-
-          Lemma wf_interp_ident G {t} idc1 idc2 (Hidc : idc1 = idc2)
-            : wf_value_with_lets G (@interp_ident1 t idc1) (@interp_ident2 t idc2).
-          Proof.
-            cbv [wf_value_with_lets ident.interp_ident]; subst idc2; destruct idc1;
-              first [ apply wf_interp_ident_nth_default
-                    | apply wf_interp_ident_not_nth_default ].
-          Qed.
-
-          Local Notation eval_with_bound1 := (@partial.ident.eval_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
-          Local Notation eval_with_bound2 := (@partial.ident.eval_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
-          Lemma wf_eval_with_bound {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
-                (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
-            : expr.wf G' (@eval_with_bound1 t e1 st1) (@eval_with_bound2 t e2 st2).
-          Proof.
-            eapply wf_eval_with_bound';
-              solve [ eassumption
-                    | eapply wf_annotate
-                    | eapply wf_interp_ident ].
-          Qed.
-
-          Local Notation eval1 := (@partial.ident.eval var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
-          Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
-          Lemma wf_eval {t} G G' e1 e2 (Hwf : expr.wf G e1 e2)
-                (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
-            : expr.wf G' (@eval1 t e1) (@eval2 t e2).
-          Proof.
-            eapply wf_eval';
-              solve [ eassumption
-                    | eapply wf_annotate
-                    | eapply wf_interp_ident ].
-          Qed.
+        Section extract.
+          Local Notation extract := (@ident.extract abstract_domain' abstract_interp_ident).
 
-          Local Notation eta_expand_with_bound1 := (@partial.ident.eta_expand_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
-          Local Notation eta_expand_with_bound2 := (@partial.ident.eta_expand_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
-          Lemma wf_eta_expand_with_bound {t} G e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
-            : expr.wf G (@eta_expand_with_bound1 t e1 st1) (@eta_expand_with_bound2 t e2 st2).
-          Proof.
-            eapply wf_eta_expand_with_bound';
-              solve [ eassumption
-                    | eapply wf_annotate
-                    | eapply wf_interp_ident ].
+          Lemma extract_Proper G
+                (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> @abstract_domain_R t v1 v2)
+                {t}
+            : Proper (expr.wf G ==> type.and_for_each_lhs_of_arrow (@abstract_domain_R) ==> abstract_domain'_R (type.final_codomain t)) (@extract t).
+          Proof using abstract_interp_ident_Proper.
+            apply @extract_gen_Proper; eauto.
           Qed.
-
-          Section extract.
-          (*
-            Definition extract {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t)
-              := @extract_gen base.type ident abstract_domain' (@ident_extract) t e bound.
-           *)
-          End extract.
-        End with_var2.
+        End extract.
       End with_type.
     End ident.
 
@@ -778,12 +129,6 @@ Module Compilers.
       Definition abstraction_relation' {t} : abstract_domain' t -> base.interp t -> Prop
         := fun st v => @ZRange.type.base.option.is_bounded_by t st v = true.
 
-      Global Instance annotate_ident_Proper {t} : Proper (abstract_domain'_R t ==> eq) (annotate_ident t).
-      Proof.
-        intros st st' ?; subst st'.
-        cbv [annotate_ident]; break_innermost_match; reflexivity.
-      Qed.
-
       Lemma interp_annotate_ident {t} st idc
             (Hst : @annotate_ident t st = Some idc)
         : forall v, abstraction_relation' st v
@@ -800,41 +145,12 @@ Module Compilers.
         : @annotate_ident t st1 = @annotate_ident t st2.
       Proof. congruence. Qed.
 
-      Global Instance bottom'_Proper {t} : Proper (abstract_domain'_R t) (bottom' t).
-      Proof. reflexivity. Qed.
-
       Lemma bottom'_bottom {t} : forall v, abstraction_relation' (bottom' t) v.
       Proof.
         cbv [abstraction_relation' bottom']; induction t; cbn; intros; break_innermost_match; cbn; try reflexivity.
         rewrite Bool.andb_true_iff; split; auto.
       Qed.
 
-      Global Instance abstract_interp_ident_Proper {t}
-        : Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t).
-      Proof.
-        cbv [abstract_interp_ident abstract_domain_R type.related respectful type.interp]; intros idc idc' ?; subst idc'; destruct idc;
-          repeat first [ reflexivity
-                       | progress subst
-                       | progress cbn [ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp Option.bind] in *
-                       | progress cbv [Option.bind]
-                       | intro
-                       | progress destruct_head'_prod
-                       | progress destruct_head'_bool
-                       | progress destruct_head' option
-                       | solve [ eauto ]
-                       | apply NatUtil.nat_rect_Proper_nondep
-                       | apply ListUtil.list_rect_Proper
-                       | apply ListUtil.list_case_Proper
-                       | apply ListUtil.pointwise_map
-                       | apply ListUtil.fold_right_Proper
-                       | apply ListUtil.update_nth_Proper
-                       | apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature)
-                       | cbn; apply (f_equal (@Some _))
-                       | match goal with
-                         | [ H : _ |- _ ] => erewrite H by (eauto; (eassumption || reflexivity))
-                         end ].
-      Qed.
-
       Lemma abstract_interp_ident_related {t} (idc : ident t)
         : type.related_hetero (@abstraction_relation') (@abstract_interp_ident t idc) (ident.interp idc).
       Proof.
@@ -842,10 +158,6 @@ Module Compilers.
         all: cbv [type.related_hetero ZRange.ident.option.interp ident.interp ident.gen_interp respectful_hetero type.interp ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp ZRange.type.base.option.Some].
       Admitted.
 
-      Global Instance update_literal_with_state_Proper {t}
-        : Proper (abstract_domain'_R (base.type.type_base t) ==> eq ==> eq) (update_literal_with_state t).
-      Proof. repeat intro; congruence. Qed.
-
       Lemma interp_update_literal_with_state {t : base.type.base} st v
         : @abstraction_relation' t st v -> @update_literal_with_state t st v = v.
       Proof.
@@ -853,26 +165,6 @@ Module Compilers.
           break_innermost_match; try congruence; reflexivity.
       Qed.
 
-      Global Instance extract_list_state_Proper {t}
-        : Proper (abstract_domain'_R _ ==> option_eq (SetoidList.eqlistA (@abstract_domain'_R t)))
-                 (extract_list_state t).
-      Proof.
-        intros st st' ?; subst st'; cbv [option_eq extract_list_state]; break_innermost_match; reflexivity.
-      Qed.
-
-      Lemma extract_list_state_length
-        : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2).
-      Proof.
-        intros; subst; cbv [option_map extract_list_state]; break_innermost_match; reflexivity.
-      Qed.
-      Lemma extract_list_state_rel
-        : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2.
-      Proof.
-        intros; cbv [extract_list_state] in *; subst; inversion_option; subst.
-        rewrite combine_same, List.in_map_iff in *.
-        destruct_head'_ex; destruct_head'_and; inversion_prod; subst; reflexivity.
-      Qed.
-
       Lemma extract_list_state_related {t} st v ls
         : @abstraction_relation' _ st v
           -> @extract_list_state t st = Some ls
@@ -889,77 +181,22 @@ Module Compilers.
           intros; destruct_head'_and; destruct_head'_or; inversion_prod; subst; eauto. }
       Qed.
 
-      Section with_var2.
-        Context {var1 var2 : type -> Type}.
-        Local Notation wf_value_with_lets := (@wf_value_with_lets base.type ident abstract_domain' (fun t => abstract_domain'_R t) var1 var2).
-
-        Lemma wf_eval {t} G G' e1 e2 (Hwf : expr.wf G e1 e2)
-              (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
-          : expr.wf G' (@eval var1 t e1) (@eval var2 t e2).
-        Proof.
-          eapply ident.wf_eval;
-            solve [ eassumption
-                  | exact _
-                  | apply extract_list_state_length
-                  | apply extract_list_state_rel ].
-        Qed.
-
-        Lemma wf_eval_with_bound {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
-              (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
-          : expr.wf G' (@eval_with_bound var1 t e1 st1) (@eval_with_bound var2 t e2 st2).
-        Proof.
-          eapply ident.wf_eval_with_bound;
-            solve [ eassumption
-                  | exact _
-                  | apply extract_list_state_length
-                  | apply extract_list_state_rel ].
-        Qed.
-
-
-        Lemma wf_eta_expand_with_bound {t} G e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
-          : expr.wf G (@eta_expand_with_bound var1 t e1 st1) (@eta_expand_with_bound var2 t e2 st2).
-        Proof.
-          eapply ident.wf_eta_expand_with_bound;
-            solve [ eassumption
-                  | exact _
-                  | apply extract_list_state_length
-                  | apply extract_list_state_rel ].
-        Qed.
-      End with_var2.
-
-      Lemma Wf_Eval {t} (e : Expr t) (Hwf : Wf e) : Wf (Eval e).
-      Proof.
-        intros ??; eapply wf_eval with (G:=nil); cbn [List.In]; try apply Hwf; tauto.
-      Qed.
-
-      Lemma Wf_EvalWithBound {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound)
-        : Wf (EvalWithBound e bound).
+      Lemma Extract_FromFlat_ToFlat' {t} (e : Expr t) (Hwf : Wf e) b_in1 b_in2
+            (Hb : type.and_for_each_lhs_of_arrow (fun t => type.eqv) b_in1 b_in2)
+        : partial.Extract (GeneralizeVar.FromFlat (GeneralizeVar.ToFlat e)) b_in1
+          = partial.Extract e b_in2.
       Proof.
-        intros ??; eapply wf_eval_with_bound with (G:=nil); cbn [List.In]; try apply Hwf; tauto.
+        cbv [partial.Extract partial.ident.extract partial.extract_gen partial.extract'].
+        revert b_in1 b_in2 Hb.
+        rewrite <- (@type.related_iff_app_curried base.type ZRange.type.base.option.interp (fun _ => eq)).
+        apply GeneralizeVar.Interp_gen1_FromFlat_ToFlat, Hwf.
       Qed.
 
-      Lemma Wf_EtaExpandWithBound {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound)
-        : Wf (EtaExpandWithBound e bound).
-      Proof.
-        intros ??; eapply wf_eta_expand_with_bound with (G:=nil); cbn [List.In]; try apply Hwf; tauto.
-      Qed.
-
-      Local Instance Proper_strip_ranges {t}
-        : Proper (@abstract_domain_R t ==> @abstract_domain_R t) (@ZRange.type.option.strip_ranges t).
-      Proof.
-        cbv [Proper abstract_domain_R respectful].
-        induction t as [t|s IHs d IHd]; cbn in *; destruct_head'_prod; destruct_head'_and; cbn in *; intros; subst; cbv [respectful] in *;
-          eauto.
-      Qed.
-
-      Lemma Wf_EtaExpandWithListInfoFromBound {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound)
-        : Wf (EtaExpandWithListInfoFromBound e bound).
-      Proof.
-        eapply Wf_EtaExpandWithBound; [ assumption | ].
-        clear dependent e.
-        cbv [Proper] in *; induction t as [t|s IHs d IHd]; cbn in *; destruct_head'_prod; destruct_head'_and; cbn in *; eauto.
-        split; auto; apply Proper_strip_ranges; auto.
-      Qed.
+      Lemma Extract_FromFlat_ToFlat {t} (e : Expr t) (Hwf : Wf e) b_in
+            (Hb : Proper (type.and_for_each_lhs_of_arrow (fun t => type.eqv)) b_in)
+        : partial.Extract (GeneralizeVar.FromFlat (GeneralizeVar.ToFlat e)) b_in
+          = partial.Extract e b_in.
+      Proof. apply Extract_FromFlat_ToFlat'; assumption. Qed.
     End specialized.
   End partial.
   Import defaults.
@@ -1026,35 +263,6 @@ Module Compilers.
                 (Hrelax : forall r r' z, is_tighter_than_bool z r = true
                                          -> relax_zrange r = Some r'
                                          -> is_tighter_than_bool z r' = true).
-        Section with_var2.
-          Context {var1 var2 : type -> Type}.
-
-          Lemma wf_relax G {t} (e1 : @expr var1 t) (e2 : @expr var2 t)
-                (Hwf : expr.wf G e1 e2)
-            : expr.wf G (@RelaxZRange.expr.relax relax_zrange var1 t e1) (@RelaxZRange.expr.relax relax_zrange var2 t e2).
-          Proof using Type.
-            clear -Hwf.
-            induction Hwf; wf_safe_t.
-            cbn [RelaxZRange.expr.relax]; cbv [option_map] in *.
-            break_innermost_match;
-              repeat first [ progress wf_safe_t
-                           | progress expr.invert_subst
-                           | progress expr.inversion_wf_constr
-                           | progress destruct_head' False
-                           | progress inversion_option
-                           | progress cbn [invert_Ident invert_Var invert_Abs invert_App invert_LetIn] in *
-                           | match goal with
-                             | [ H : context[RelaxZRange.expr.relax ?r ?x], H' : RelaxZRange.expr.relax ?r ?x = _ |- _ ]
-                               => rewrite H' in H
-                             | [ H : context[match RelaxZRange.expr.relax ?r ?x with _ => _ end] |- _ ]
-                               => remember (RelaxZRange.expr.relax r x) in *; progress expr.invert_match
-                             | [ H : ?x = Some ?a, H' : context[?x] |- _ ] => rewrite H in H'
-                             | [ H : ?x = None, H' : context[?x] |- _ ] => rewrite H in H'
-                             end
-                           | progress expr.inversion_wf_one_constr ].
-          Qed.
-        End with_var2.
-
         Lemma interp_relax {t} (e : expr t)
               v
               (Hinterp : forall cast_outside_of_range, type.app_curried (expr.interp (@ident.gen_interp cast_outside_of_range) e) v
@@ -1103,8 +311,6 @@ Module Compilers.
                               end ].
         Admitted.
 
-        Lemma Wf_Relax {t} (e : Expr t) (Hwf : Wf e) : Wf (@RelaxZRange.expr.Relax relax_zrange t e).
-        Proof. intros ??; eapply wf_relax, Hwf. Qed.
         Lemma Interp_Relax {t} (e : Expr t)
               v
               (Hinterp : forall cast_outside_of_range, type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) e) v
@@ -1120,23 +326,31 @@ Module Compilers.
   Axiom admit_pf : False.
   Local Notation admit := (match admit_pf with end).
 
-  Lemma Wf_PartialEvaluateWithListInfoFromBounds
+  Lemma Interp_PartialEvaluateWithBounds
+        cast_outside_of_range
         {t} (E : Expr t)
-        (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
         (Hwf : Wf E)
-        {b_in_Proper : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R base.type ZRange.type.base.option.interp (fun t0 : base.type => eq))) b_in}
-    : Wf (PartialEvaluateWithListInfoFromBounds E b_in).
-  Proof. apply Wf_EtaExpandWithListInfoFromBound; assumption. Qed.
-  Hint Resolve Wf_PartialEvaluateWithListInfoFromBounds : wf.
+        (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
+    : forall arg1 arg2
+        (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
+        (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
+      type.app_curried (expr.Interp (@ident.gen_interp cast_outside_of_range) (PartialEvaluateWithBounds E b_in)) arg1
+      = type.app_curried (Interp E) arg2.
+  Proof.
+  Admitted.
 
-  Lemma Wf_PartialEvaluateWithBounds
+  Lemma Interp_PartialEvaluateWithBounds_bounded
         {t} (E : Expr t)
-        (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
         (Hwf : Wf E)
-        {b_in_Proper : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R base.type ZRange.type.base.option.interp (fun t0 : base.type => eq))) b_in}
-    : Wf (PartialEvaluateWithBounds E b_in).
-  Proof. eapply partial.Wf_EvalWithBound; assumption. Qed.
-  Hint Resolve Wf_PartialEvaluateWithBounds : wf.
+        (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
+    : forall arg1
+        (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) b_in arg1 = true),
+      ZRange.type.base.option.is_bounded_by
+        (partial.Extract (PartialEvaluateWithBounds E b_in) b_in)
+        (type.app_curried (expr.Interp (@ident.interp) (PartialEvaluateWithBounds E b_in)) arg1)
+      = true.
+  Proof.
+  Admitted.
 
   Lemma Interp_PartialEvaluateWithListInfoFromBounds
         {t} (E : Expr t)
@@ -1149,8 +363,6 @@ Module Compilers.
   Proof.
   Admitted.
 
-  Hint Resolve Wf_EtaExpandWithBound Wf_PartialEvaluateWithListInfoFromBounds : wf.
-
   Theorem CheckedPartialEvaluateWithBounds_Correct
           (relax_zrange : zrange -> option zrange)
           (Hrelax : forall r r' z, is_tighter_than_bool z r = true
@@ -1174,16 +386,18 @@ Module Compilers.
       break_innermost_match_hyps; inversion_sum; subst.
     split.
     { intros arg1 arg2 Harg12 Harg1.
+      assert (arg1_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related base.type base.interp (fun _ => eq))) arg1)
+        by (hnf; etransitivity; [ eassumption | symmetry; eassumption ]).
       split.
-      { eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ].
-        clear dependent arg2.
-        cbv [ident.interp]; rewrite RelaxZRange.expr.Interp_Relax; eauto.
-        all: revert Harg1.
-        all: exact admit. (* boundedness *) }
-      { intro cast_outside_of_range; revert cast_outside_of_range Harg12.
-        intros ? Harg; rewrite RelaxZRange.expr.Interp_Relax; eauto.
-        all: revert Harg.
-        all: exact admit. (* correctness of interp *) } }
+      all: repeat first [ rewrite !@GeneralizeVar.Interp_gen1_FromFlat_ToFlat by eauto with wf typeclass_instances
+                        | rewrite Extract_FromFlat_ToFlat by auto with wf
+                        | eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ]
+                        | apply Interp_PartialEvaluateWithBounds_bounded; auto
+                        | progress cbv [ident.interp]
+                        | rewrite RelaxZRange.expr.Interp_Relax; eauto
+                        | erewrite !Interp_PartialEvaluateWithBounds
+                        | solve [ eauto ]
+                        | progress intros ]. }
     { auto with wf. }
   Qed.
 End Compilers.
diff --git a/src/Experiments/NewPipeline/AbstractInterpretationWf.v b/src/Experiments/NewPipeline/AbstractInterpretationWf.v
new file mode 100644
index 000000000..ecd52ddec
--- /dev/null
+++ b/src/Experiments/NewPipeline/AbstractInterpretationWf.v
@@ -0,0 +1,825 @@
+Require Import Coq.micromega.Lia.
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.Classes.Morphisms.
+Require Import Coq.Classes.RelationPairs.
+Require Import Coq.Relations.Relations.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.Sum.
+Require Import Crypto.Util.LetIn.
+Require Import Crypto.Util.Prod.
+Require Import Crypto.Util.Sigma.
+Require Import Crypto.Util.Option.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.NatUtil.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.SplitInContext.
+Require Import Crypto.Util.Tactics.UniquePose.
+Require Import Crypto.Util.Tactics.SpecializeBy.
+Require Import Crypto.Util.Tactics.SpecializeAllWays.
+Require Import Crypto.Experiments.NewPipeline.Language.
+Require Import Crypto.Experiments.NewPipeline.LanguageInversion.
+Require Import Crypto.Experiments.NewPipeline.LanguageWf.
+Require Import Crypto.Experiments.NewPipeline.UnderLetsProofs.
+Require Import Crypto.Experiments.NewPipeline.AbstractInterpretation.
+
+Module Compilers.
+  Import Language.Compilers.
+  Import UnderLets.Compilers.
+  Import AbstractInterpretation.Compilers.
+  Import LanguageInversion.Compilers.
+  Import LanguageWf.Compilers.
+  Import UnderLetsProofs.Compilers.
+  Import invert_expr.
+
+  Module Import partial.
+    Import AbstractInterpretation.Compilers.partial.
+    Import NewPipeline.UnderLets.Compilers.UnderLets.
+    Section with_type.
+      Context {base_type : Type}.
+      Local Notation type := (type base_type).
+      Let type_base (x : base_type) : type := type.base x.
+      Local Coercion type_base : base_type >-> type.
+      Context {ident : type -> Type}.
+      Local Notation expr := (@expr base_type ident).
+      Local Notation Expr := (@expr.Expr base_type ident).
+      Local Notation UnderLets := (@UnderLets base_type ident).
+      Context (abstract_domain' : base_type -> Type)
+              (bottom' : forall A, abstract_domain' A)
+              (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t)
+              (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop)
+              {abstract_interp_ident_Proper : forall t, Proper (eq ==> abstract_domain'_R t) (abstract_interp_ident t)}
+              {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)}.
+      Local Notation abstract_domain := (@abstract_domain base_type abstract_domain').
+      Local Notation bottom := (@bottom base_type abstract_domain' (@bottom')).
+      Local Notation bottom_for_each_lhs_of_arrow := (@bottom_for_each_lhs_of_arrow base_type abstract_domain' (@bottom')).
+
+      Section with_var2.
+        Context {var1 var2 : type -> Type}.
+        Local Notation UnderLets1 := (@UnderLets.UnderLets base_type ident var1).
+        Local Notation UnderLets2 := (@UnderLets.UnderLets base_type ident var2).
+        Local Notation expr1 := (@expr.expr base_type ident var1).
+        Local Notation expr2 := (@expr.expr base_type ident var2).
+        Local Notation value1 := (@value base_type ident var1 abstract_domain').
+        Local Notation value2 := (@value base_type ident var2 abstract_domain').
+        Local Notation value_with_lets1 := (@value_with_lets base_type ident var1 abstract_domain').
+        Local Notation value_with_lets2 := (@value_with_lets base_type ident var2 abstract_domain').
+        Local Notation state_of_value1 := (@state_of_value base_type ident var1 abstract_domain').
+        Local Notation state_of_value2 := (@state_of_value base_type ident var2 abstract_domain').
+        Context (annotate1 : forall (is_let_bound : bool) t, abstract_domain' t -> @expr1 t -> UnderLets1 (@expr1 t))
+                (annotate2 : forall (is_let_bound : bool) t, abstract_domain' t -> @expr2 t -> UnderLets2 (@expr2 t))
+                (annotate_Proper
+                 : forall is_let_bound t G
+                     v1 v2 (Hv : abstract_domain'_R t v1 v2)
+                     e1 e2 (He : expr.wf G e1 e2),
+                    UnderLets.wf (fun G' => expr.wf G') G (annotate1 is_let_bound t v1 e1) (annotate2 is_let_bound t v2 e2))
+                (interp_ident1 : forall t, ident t -> value_with_lets1 t)
+                (interp_ident2 : forall t, ident t -> value_with_lets2 t).
+        Local Notation reify1 := (@reify base_type ident var1 abstract_domain' annotate1 bottom').
+        Local Notation reify2 := (@reify base_type ident var2 abstract_domain' annotate2 bottom').
+        Local Notation reflect1 := (@reflect base_type ident var1 abstract_domain' annotate1 bottom').
+        Local Notation reflect2 := (@reflect base_type ident var2 abstract_domain' annotate2 bottom').
+        Local Notation interp1 := (@interp base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1).
+        Local Notation interp2 := (@interp base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2).
+        Local Notation eval_with_bound'1 := (@eval_with_bound' base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1).
+        Local Notation eval_with_bound'2 := (@eval_with_bound' base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2).
+        Local Notation eval'1 := (@eval' base_type ident var1 abstract_domain' annotate1 bottom' interp_ident1).
+        Local Notation eval'2 := (@eval' base_type ident var2 abstract_domain' annotate2 bottom' interp_ident2).
+        Local Notation eta_expand_with_bound'1 := (@eta_expand_with_bound' base_type ident var1 abstract_domain' annotate1 bottom').
+        Local Notation eta_expand_with_bound'2 := (@eta_expand_with_bound' base_type ident var2 abstract_domain' annotate2 bottom').
+
+        Definition abstract_domain_R {t} : relation (abstract_domain t)
+          := type.related abstract_domain'_R.
+
+        (** This one is tricky.  Because we need to be stable under
+            weakening and reordering of the context, we permit any
+            context for well-formedness of the input in the arrow
+            case, and simply tack on that context at the beginning of
+            the output.  This is sort-of wasteful on the output
+            context, but it's sufficient to prove
+            [wf_value_Proper_list] below, which is what we really
+            need. *)
+        Fixpoint wf_value G {t} : value1 t -> value2 t -> Prop
+          := match t return value1 t -> value2 t -> Prop with
+             | type.base t
+               => fun v1 v2
+                 => abstract_domain_R (fst v1) (fst v2)
+                   /\ expr.wf G (snd v1) (snd v2)
+             | type.arrow s d
+               => fun v1 v2
+                 => abstract_domain_R (fst v1) (fst v2)
+                   /\ (forall seg G' sv1 sv2,
+                         G' = (seg ++ G)%list
+                         -> @wf_value seg s sv1 sv2
+                         -> UnderLets.wf
+                             (fun G' => @wf_value G' d) G'
+                             (snd v1 sv1) (snd v2 sv2))
+             end.
+
+        Definition wf_value_with_lets G {t} : value_with_lets1 t -> value_with_lets2 t -> Prop
+          := UnderLets.wf (fun G' => wf_value G') G.
+
+        Context (interp_ident_Proper
+                 : forall G t idc1 idc2 (Hidc : idc1 = idc2),
+                    wf_value_with_lets G (interp_ident1 t idc1) (interp_ident2 t idc2)).
+
+        Global Instance bottom_Proper {t} : Proper abstract_domain_R (@bottom t) | 10.
+        Proof using bottom'_Proper.
+          clear -bottom'_Proper type_base.
+          cbv [Proper] in *; induction t; cbn; cbv [respectful]; eauto.
+        Qed.
+
+        Global Instance bottom_for_each_lhs_of_arrow_Proper {t}
+          : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) (@bottom_for_each_lhs_of_arrow t) | 10.
+        Proof using bottom'_Proper.
+          clear -bottom'_Proper type_base.
+          pose proof (@bottom_Proper).
+          cbv [Proper] in *; induction t; cbn; cbv [respectful]; eauto.
+        Qed.
+
+        Lemma state_of_value_Proper G {t} v1 v2 (Hv : @wf_value G t v1 v2)
+          : abstract_domain_R (state_of_value1 v1) (state_of_value2 v2).
+        Proof using Type.
+          clear -Hv type_base.
+          destruct t, v1, v2, Hv; cbn in *; cbv [respectful]; eauto.
+        Qed.
+
+        Local Hint Resolve (ex_intro _ nil) (ex_intro _ (cons _ nil)).
+        Local Hint Constructors expr.wf ex.
+        Local Hint Unfold List.In.
+
+        Lemma wf_value_Proper_list G1 G2
+              (HG1G2 : forall t v1 v2, List.In (existT _ t (v1, v2)) G1 -> List.In (existT _ t (v1, v2)) G2)
+              t e1 e2
+              (Hwf : @wf_value G1 t e1 e2)
+          : @wf_value G2 t e1 e2.
+        Proof using Type.
+          clear -type_base HG1G2 Hwf.
+          revert dependent G1; revert dependent G2; induction t; intros;
+            repeat first [ progress cbn in *
+                         | progress intros
+                         | solve [ eauto ]
+                         | progress subst
+                         | progress destruct_head'_and
+                         | progress destruct_head'_or
+                         | apply conj
+                         | rewrite List.in_app_iff in *
+                         | match goal with H : _ |- _ => apply H; clear H end
+                         | wf_unsafe_t_step
+                         | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ] ].
+        Qed.
+
+        Fixpoint wf_reify (is_let_bound : bool) G {t}
+          : forall v1 v2 (Hv : @wf_value G t v1 v2)
+              s1 s2 (Hs : type.and_for_each_lhs_of_arrow (@abstract_domain_R) s1 s2),
+            UnderLets.wf (fun G' => expr.wf G') G (@reify1 is_let_bound t v1 s1) (@reify2 is_let_bound t v2 s2)
+        with wf_reflect G {t}
+             : forall e1 e2 (He : expr.wf G e1 e2)
+                 s1 s2 (Hs : abstract_domain_R s1 s2),
+            @wf_value G t (@reflect1 t e1 s1) (@reflect2 t e2 s2).
+        Proof using annotate_Proper bottom'_Proper.
+          all: clear -wf_reflect wf_reify annotate_Proper type_base bottom'_Proper.
+          all: pose proof (@bottom_for_each_lhs_of_arrow_Proper); cbv [Proper] in *.
+          { destruct t as [t|s d];
+              [ clear wf_reify wf_reflect
+              | specialize (fun G => wf_reflect G s);
+                specialize (fun G => wf_reify false G d) ].
+            { cbn; intros [? ?] [? ?] [Hv0 Hv1] [] [] [];
+                cbn [fst snd] in *.
+              apply annotate_Proper; assumption. }
+            { cbn; cbv [respectful]; intros [? ?] [? ?] [He0 He1] [? ?] [? ?] [Hs0 Hs1];
+                cbn [fst snd] in *.
+              do 2 constructor; intros v1 v2.
+              eapply UnderLets.wf_to_expr, UnderLets.wf_splice.
+              { eapply He1 with (seg:=cons _ nil); eauto using eq_refl. }
+              { intros; apply wf_reify; destruct_head'_ex; subst; auto. } } }
+          { destruct t as [t|s d];
+              [ clear wf_reify wf_reflect
+              | specialize (fun G => wf_reflect G d);
+                specialize (fun G => wf_reify false G s) ].
+            { cbn; auto. }
+            { cbn; cbv [respectful]; intros e1 e2 He s1 s2 Hs;
+                split; [ solve [ auto ] | ];
+                  intros G' seg sv1 sv2 HG1G2 Hsv; subst.
+              eapply UnderLets.wf_splice.
+              { apply wf_reify; auto; eapply wf_value_Proper_list; [ .. | solve [ eauto ] ];
+                  wf_safe_t. }
+              { intros G'' a1 a2 [seg' ?] Ha; subst G''.
+                constructor.
+                apply wf_reflect.
+                { constructor; auto; wf_unsafe_t_step; [].
+                  destruct_head'_ex; subst.
+                  intros *.
+                  rewrite !List.in_app_iff; auto. }
+                { eapply Hs, state_of_value_Proper; eassumption. } } } }
+        Qed.
+
+        Local Ltac wf_interp_t :=
+          repeat first [ progress cbv [wf_value_with_lets abstract_domain_R respectful] in *
+                       | progress cbn [wf_value fst snd partial.bottom type.related eq_rect List.In] in *
+                       | wf_safe_t_step
+                       | exact I
+                       | apply wf_reify
+                       | apply bottom_Proper
+                       | progress destruct_head'_ex
+                       | progress destruct_head'_or
+                       | eapply UnderLets.wf_splice
+                       | match goal with
+                         | [ |- UnderLets.wf _ _ _ _ ] => constructor
+                         | [ |- and _ _ ] => apply conj
+                         end
+                       | eapply wf_value_Proper_list; [ | solve [ eauto ] ]
+                       | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ]
+                       | match goal with
+                         | [ H : _ |- _ ] => eapply H; clear H; solve [ wf_interp_t ]
+                         end
+                       | break_innermost_match_step ].
+
+        Lemma wf_interp G G' {t} (e1 : @expr (@value_with_lets1) t) (e2 : @expr (@value_with_lets2) t)
+              (Hwf : expr.wf G e1 e2)
+              (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
+          : wf_value_with_lets G' (interp1 e1) (interp2 e2).
+        Proof using annotate_Proper bottom'_Proper interp_ident_Proper.
+          revert dependent G'; induction Hwf; intros; cbn [interp];
+            try solve [ apply interp_ident_Proper; auto
+                      | eauto ];
+            wf_interp_t.
+        Qed.
+
+        Lemma wf_eval_with_bound' G G' {t} e1 e2 (He : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
+              (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
+          : expr.wf G' (@eval_with_bound'1 t e1 st1) (@eval_with_bound'2 t e2 st2).
+        Proof using annotate_Proper bottom'_Proper interp_ident_Proper.
+          eapply UnderLets.wf_to_expr, UnderLets.wf_splice.
+          { eapply wf_interp; solve [ eauto ]. }
+          { intros; destruct_head'_ex; subst; eapply wf_reify; eauto. }
+        Qed.
+
+        Lemma wf_eval' G G' {t} e1 e2 (He : expr.wf G e1 e2)
+              (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
+          : expr.wf G' (@eval'1 t e1) (@eval'2 t e2).
+        Proof using annotate_Proper bottom'_Proper interp_ident_Proper.
+          eapply wf_eval_with_bound'; eauto; apply bottom_for_each_lhs_of_arrow_Proper.
+        Qed.
+
+        Lemma wf_eta_expand_with_bound' G {t} e1 e2 (He : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
+          : expr.wf G (@eta_expand_with_bound'1 t e1 st1) (@eta_expand_with_bound'2 t e2 st2).
+        Proof using annotate_Proper bottom'_Proper.
+          eapply UnderLets.wf_to_expr, wf_reify; [ eapply wf_reflect | ]; eauto; apply bottom_Proper.
+        Qed.
+      End with_var2.
+    End with_type.
+
+    Module ident.
+      Import defaults.
+      Local Notation UnderLets := (@UnderLets base.type ident).
+      Section with_type.
+        Context (abstract_domain' : base.type -> Type).
+        Local Notation abstract_domain := (@abstract_domain base.type abstract_domain').
+        Context (annotate_ident : forall t, abstract_domain' t -> option (ident (t -> t)))
+                (bottom' : forall A, abstract_domain' A)
+                (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t)
+                (update_literal_with_state : forall A : base.type.base, abstract_domain' A -> base.interp A -> base.interp A)
+                (extract_list_state : forall A, abstract_domain' (base.type.list A) -> option (list (abstract_domain' A)))
+                (is_annotation : forall t, ident t -> bool).
+        Context (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop).
+        Local Notation abstract_domain_R := (@abstract_domain_R base.type abstract_domain' abstract_domain'_R).
+        Context {annotate_ident_Proper : forall t, Proper (abstract_domain'_R t ==> eq) (annotate_ident t)}
+                {abstract_interp_ident_Proper : forall t, Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t)}
+                {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)}
+                {update_literal_with_state_Proper : forall t, Proper (abstract_domain'_R (base.type.type_base t) ==> eq ==> eq) (update_literal_with_state t)}
+                (extract_list_state_length : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2))
+                (extract_list_state_rel : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2).
+
+        Local Instance abstract_interp_ident_Proper_arrow s d
+          : Proper (eq ==> abstract_domain'_R s ==> abstract_domain'_R d) (abstract_interp_ident (type.arrow s d))
+          := abstract_interp_ident_Proper (type.arrow s d).
+
+        Section with_var2.
+          Context {var1 var2 : type -> Type}.
+
+          Local Notation update_annotation1 := (@ident.update_annotation var1 abstract_domain' annotate_ident abstract_interp_ident is_annotation).
+          Local Notation update_annotation2 := (@ident.update_annotation var2 abstract_domain' annotate_ident abstract_interp_ident is_annotation).
+          Local Notation annotate1 := (@ident.annotate var1 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
+          Local Notation annotate2 := (@ident.annotate var2 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
+          Local Notation annotate_base1 := (@ident.annotate_base var1 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state is_annotation).
+          Local Notation annotate_base2 := (@ident.annotate_base var2 abstract_domain' annotate_ident abstract_interp_ident update_literal_with_state is_annotation).
+          Local Notation annotate_with_ident1 := (@ident.annotate_with_ident var1 abstract_domain' annotate_ident abstract_interp_ident is_annotation).
+          Local Notation annotate_with_ident2 := (@ident.annotate_with_ident var2 abstract_domain' annotate_ident abstract_interp_ident is_annotation).
+          Local Notation interp_ident1 := (@ident.interp_ident var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
+          Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
+          Local Notation reflect1 := (@reflect base.type ident var1 abstract_domain' annotate1 bottom').
+          Local Notation reflect2 := (@reflect base.type ident var2 abstract_domain' annotate2 bottom').
+
+          Lemma wf_update_annotation G {t} st1 st2 (Hst : abstract_domain'_R t st1 st2) e1 e2 (He : expr.wf G e1 e2)
+            : expr.wf G (@update_annotation1 t st1 e1) (@update_annotation2 t st2 e2).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper.
+            cbv [ident.update_annotation];
+              repeat first [ progress subst
+                           | progress expr.invert_subst
+                           | progress cbn [fst snd projT1 projT2 eq_rect] in *
+                           | progress cbn [invert_AppIdent Option.bind invert_App invert_Ident] in *
+                           | progress destruct_head'_sig
+                           | progress destruct_head'_sigT
+                           | progress destruct_head'_and
+                           | progress destruct_head'_prod
+                           | progress destruct_head' False
+                           | progress inversion_option
+                           | progress expr.inversion_wf_constr
+                           | progress expr.inversion_wf_one_constr
+                           | break_innermost_match_hyps_step
+                           | expr.invert_match_step
+                           | progress expr.inversion_expr
+                           | progress rewrite_type_transport_correct
+                           | progress type_beq_to_eq
+                           | progress type.inversion_type
+                           | progress base.type.inversion_type
+                           | match goal with
+                             | [ H : abstract_domain'_R _ ?x _ |- _ ] => rewrite !H; clear dependent x
+                             end
+                           | progress wf_safe_t
+                           | break_innermost_match_step ].
+          Qed.
+
+          Lemma wf_annotate_with_ident
+                is_let_bound t G
+                v1 v2 (Hv : abstract_domain'_R t v1 v2)
+                e1 e2 (He : expr.wf G e1 e2)
+            : UnderLets.wf (fun G' => expr.wf G') G (@annotate_with_ident1 is_let_bound t v1 e1) (@annotate_with_ident2 is_let_bound t v2 e2).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper.
+            cbv [ident.annotate_with_ident]; break_innermost_match; repeat constructor; apply wf_update_annotation; assumption.
+          Qed.
+
+          Lemma wf_annotate_base
+                is_let_bound (t : base.type.base) G
+                v1 v2 (Hv : abstract_domain'_R t v1 v2)
+                e1 e2 (He : expr.wf G e1 e2)
+            : UnderLets.wf (fun G' => expr.wf G') G (@annotate_base1 is_let_bound t v1 e1) (@annotate_base2 is_let_bound t v2 e2).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper update_literal_with_state_Proper.
+            cbv [ident.annotate_base];
+              repeat first [ apply wf_annotate_with_ident
+                           | break_innermost_match_step
+                           | progress subst
+                           | progress cbv [type_base ident.smart_Literal] in *
+                           | progress cbn [invert_Literal ident.invert_Literal] in *
+                           | discriminate
+                           | progress destruct_head' False
+                           | progress expr.invert_subst
+                           | progress expr.inversion_wf
+                           | wf_safe_t_step
+                           | break_innermost_match_hyps_step
+                           | match goal with
+                             | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H
+                             | [ |- UnderLets.wf _ _ _ _ ] => constructor
+                             | [ H : abstract_domain'_R _ _ _ |- _ ] => rewrite !H
+                             end
+                           | progress expr.invert_match_step
+                           | progress expr.inversion_expr ].
+          Qed.
+
+          Lemma wf_annotate
+                is_let_bound t G
+                v1 v2 (Hv : abstract_domain'_R t v1 v2)
+                e1 e2 (He : expr.wf G e1 e2)
+            : UnderLets.wf (fun G' => expr.wf G') G (@annotate1 is_let_bound t v1 e1) (@annotate2 is_let_bound t v2 e2).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper.
+            revert dependent G; induction t; intros;
+              cbn [ident.annotate]; try apply wf_annotate_base; trivial.
+            all: repeat first [ lazymatch goal with
+                                | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e1 = Some _, H'' : reflect_list ?e2 = None |- _ ]
+                                  => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence
+                                | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e2 = Some _, H'' : reflect_list ?e1 = None |- _ ]
+                                  => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence
+                                | [ H : expr.wf _ (reify_list _) (reify_list _) |- _ ] => apply expr.wf_reify_list in H
+                                | [ |- expr.wf _ (reify_list _) (reify_list _) ] => apply expr.wf_reify_list
+                                | [ |- UnderLets.wf _ _ (UnderLets.splice_list _ _) (UnderLets.splice_list _ _) ]
+                                  => eapply @UnderLets.wf_splice_list_no_order with (P:=fun G => expr.wf G); autorewrite with distr_length
+                                | [ H : expr.wf _ (reify_list _) ?e, H' : reflect_list ?e = None |- _ ]
+                                  => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence
+                                | [ H : expr.wf _ ?e (reify_list _), H' : reflect_list ?e = None |- _ ]
+                                  => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence
+                                | [ H : extract_list_state ?t ?v1 = ?x1, H' : extract_list_state ?t ?v2 = ?x2, Hv : abstract_domain'_R _ ?v1 ?v2 |- _ ]
+                                  => let Hl := fresh in
+                                     let Hl' := fresh in
+                                     pose proof (extract_list_state_length _ v1 v2 Hv) as Hl;
+                                     pose proof (extract_list_state_rel _ v1 v2 Hv) as Hl';
+                                     rewrite H, H' in Hl, Hl'; cbv [option_eq option_map] in Hl, Hl'; clear H H'
+                                | [ H : ?x = ?x |- _ ] => clear H
+                                | [ H : length ?l1 = length ?l2, H' : context[length ?l1] |- _ ] => rewrite H in H'
+                                end
+                              | apply wf_annotate_with_ident
+                              | apply DefaultValue.expr.base.wf_default
+                              | apply DefaultValue.expr.wf_default
+                              | progress expr.invert_subst
+                              | progress cbn [ident.annotate ident.smart_Literal invert_Literal ident.invert_Literal invert_pair invert_AppIdent2 invert_App2 fst snd projT2 projT1 eq_rect Option.bind] in *
+                              | progress destruct_head' False
+                              | progress inversion_option
+                              | progress destruct_head'_ex
+                              | discriminate
+                              | wf_safe_t_step
+                              | progress expr.inversion_wf_constr
+                              | progress expr.inversion_expr
+                              | progress type_beq_to_eq
+                              | progress type.inversion_type
+                              | progress base.type.inversion_type
+                              | match goal with
+                                | [ |- expr.wf _ (update_annotation1 _ _) (update_annotation2 _ _) ] => apply wf_update_annotation
+                                | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H
+                                | [ |- UnderLets.wf _ _ _ _ ] => constructor
+                                | [ H : abstract_domain'_R _ ?x _ |- _ ] => rewrite !H
+                                | [ |- UnderLets.wf _ _ (UnderLets.splice _ _) (UnderLets.splice _ _) ] => eapply UnderLets.wf_splice
+                                | [ H : List.nth_error (List.map _ _) _ = Some _ |- _ ] => apply nth_error_map in H
+                                | [ H : context[List.nth_error (List.combine _ _) _] |- _ ] => rewrite nth_error_combine in H
+                                | [ |- context[List.nth_error (List.combine _ _) _] ] => rewrite nth_error_combine
+                                | [ H : forall x y, Some _ = Some _ -> Some _ = Some _ -> _ |- _ ]
+                                  => specialize (H _ _ eq_refl eq_refl)
+                                | [ H : forall v1 v2, List.In (v1, v2) (List.combine ?l1 ?l2) -> ?R v1 v2, H' : List.nth_error ?l1 ?n = Some ?a1, H'' : List.nth_error ?l2 ?n = Some ?a2
+                                                                                                                                                  |- ?R ?a1 ?a2 ]
+                                  => apply H
+                                | [ H : List.nth_error ?l ?n' = Some ?v |- List.In (?v, _) (List.combine ?l _) ] => apply nth_error_In with (n:=n')
+                                end
+                              | break_innermost_match_step
+                              | break_innermost_match_hyps_step
+                              | progress expr.invert_match
+                              | progress expr.inversion_wf_one_constr
+                              | match goal with
+                                | [ H : context[UnderLets.wf _ _ (annotate1 _ _ _) (annotate2 _ _ _)]
+                                    |- UnderLets.wf _ _ (annotate1 _ _ _) (annotate2 _ _ _) ] => eapply H
+                                end
+                              | apply abstract_interp_ident_Proper_arrow
+                              | progress rewrite_type_transport_correct
+                              | apply conj
+                              | congruence
+                              | solve [ wf_t ] ].
+          Qed.
+
+          Local Notation wf_value_with_lets := (@wf_value_with_lets base.type ident abstract_domain' abstract_domain'_R var1 var2).
+          Local Notation wf_value := (@wf_value base.type ident abstract_domain' abstract_domain'_R var1 var2).
+
+          Lemma wf_interp_ident_nth_default G T
+            : wf_value_with_lets G (@interp_ident1 _ (@ident.List_nth_default T)) (@interp_ident2 _ (@ident.List_nth_default T)).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper.
+            cbv [wf_value_with_lets wf_value ident.interp_ident]; constructor; cbn -[abstract_domain_R abstract_domain].
+            split.
+            { exact (abstract_interp_ident_Proper _ (@ident.List_nth_default T) _ eq_refl). }
+            { intros; subst.
+              destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *.
+              repeat first [ progress subst
+                           | progress cbn [invert_Literal ident.invert_Literal] in *
+                           | lazymatch goal with
+                             | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e1 = Some _, H'' : reflect_list ?e2 = None |- _ ]
+                               => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence
+                             | [ H : expr.wf _ ?e1 ?e2, H' : reflect_list ?e2 = Some _, H'' : reflect_list ?e1 = None |- _ ]
+                               => apply expr.wf_reflect_list in H; rewrite H', H'' in H; exfalso; clear -H; intuition congruence
+                             | [ H : expr.wf _ (reify_list _) (reify_list _) |- _ ] => apply expr.wf_reify_list in H
+                             | [ |- expr.wf _ (reify_list _) (reify_list _) ] => apply expr.wf_reify_list
+                             | [ |- UnderLets.wf _ _ (UnderLets.splice_list _ _) (UnderLets.splice_list _ _) ]
+                               => eapply @UnderLets.wf_splice_list_no_order with (P:=fun G => expr.wf G); autorewrite with distr_length
+                             | [ H : expr.wf _ (reify_list _) ?e, H' : reflect_list ?e = None |- _ ]
+                               => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence
+                             | [ H : expr.wf _ ?e (reify_list _), H' : reflect_list ?e = None |- _ ]
+                               => apply expr.wf_reflect_list in H; rewrite H', expr.reflect_reify_list in H; exfalso; clear -H; intuition congruence
+                             | [ H : extract_list_state ?t ?v1 = ?x1, H' : extract_list_state ?t ?v2 = ?x2, Hv : abstract_domain_R ?v1 ?v2 |- _ ]
+                               => let Hl := fresh in
+                                  let Hl' := fresh in
+                                  pose proof (extract_list_state_length _ v1 v2 Hv) as Hl;
+                                  pose proof (extract_list_state_rel _ v1 v2 Hv) as Hl';
+                                  rewrite H, H' in Hl, Hl'; cbv [option_eq option_map] in Hl, Hl'; clear H H'
+                             | [ H : ?x = ?x |- _ ] => clear H
+                             | [ H : length ?l1 = length ?l2, H' : context[length ?l1] |- _ ] => rewrite H in H'
+                             end
+                           | match goal with
+                             | [ |- UnderLets.wf ?Q ?G (UnderLets.splice ?x1 ?e1) (UnderLets.splice ?x2 ?e2) ]
+                               => simple refine (@UnderLets.wf_splice _ _ _ _ _ _ _ _ _ Q G x1 x2 _ e1 e2 _);
+                                  [ let G := fresh "G" in
+                                    intro G;
+                                    lazymatch goal with
+                                    | [ |- (abstract_domain ?t * _) -> _ -> _ ]
+                                      => refine (@wf_value G t)
+                                    | [ |- expr _ -> _ -> _ ]
+                                      => refine (expr.wf G)
+                                    end
+                                  | | ]
+                             | [ |- UnderLets.wf ?Q ?G (UnderLets.Base _) (UnderLets.Base _) ]
+                               => constructor
+                             | [ H : _ = _ :> ident _ |- _ ] => inversion H; clear H
+                             | [ H : List.nth_error _ _ = None |- _ ] => apply List.nth_error_None in H
+                             | [ H : List.nth_error _ _ = Some _ |- _ ]
+                               => unique pose proof (@ListUtil.nth_error_value_length _ _ _ _ H);
+                                  unique pose proof (@ListUtil.nth_error_value_In _ _ _ _ H)
+                             | [ H : context[List.In _ (List.map _ _)] |- _ ] => rewrite List.in_map_iff in H
+                             | [ H : (?x <= ?y)%nat, H' : (?y < ?x)%nat |- _ ] => exfalso; clear -H H'; lia
+                             | [ H : (?x <= ?y)%nat, H' : (?y < ?x')%nat, H'' : ?x' = ?x |- _ ] => exfalso; clear -H H' H''; lia
+                             | [ H : length ?x = length ?y |- context[length ?x] ] => rewrite H
+                             | [ H : List.nth_error (List.map _ _) _ = Some _ |- _ ] => apply nth_error_map in H
+                             | [ H : context[List.nth_error (List.combine _ _) _] |- _ ] => rewrite nth_error_combine in H
+                             | [ |- context[List.nth_error (List.combine _ _) _] ] => rewrite nth_error_combine
+                             | [ H : forall x y, Some _ = Some _ -> Some _ = Some _ -> _ |- _ ]
+                               => specialize (H _ _ eq_refl eq_refl)
+                             | [ H : forall v1 v2, List.In (v1, v2) (List.combine ?l1 ?l2) -> ?R v1 v2, H' : List.nth_error ?l1 ?n' = Some ?a1, H'' : List.nth_error ?l2 ?n' = Some ?a2
+                                                                                                                                                |- _ ]
+                               => unique pose proof (H a1 a2 ltac:(apply nth_error_In with (n:=n'); rewrite nth_error_combine, H', H''; reflexivity))
+                             | [ H : List.nth_error ?l ?n' = Some ?v |- List.In (?v, _) (List.combine ?l _) ] => apply nth_error_In with (n:=n')
+                             | [ H : context[length ?ls] |- _ ] => tryif is_var ls then fail else (progress autorewrite with distr_length in H)
+                             | [ H : context[List.nth_error (List.seq _ _) _] |- _ ] => rewrite nth_error_seq in H
+                             end
+                           | progress inversion_option
+                           | progress intros
+                           | progress cbn [fst snd value] in *
+                           | progress destruct_head'_prod
+                           | progress destruct_head'_ex
+                           | progress destruct_head'_and
+                           | progress destruct_head' False
+                           | progress specialize_by_assumption
+                           | apply conj
+                           | progress expr.invert_subst
+                           | progress expr.inversion_wf_constr
+                           | progress expr.inversion_expr
+                           | wf_safe_t_step
+                           | progress destruct_head' (@partial.wf_value)
+                           | solve [ eapply wf_annotate; wf_t; try apply DefaultValue.expr.base.wf_default
+                                   | eapply wf_annotate_base; wf_t
+                                   | eapply (abstract_interp_ident_Proper _ (@ident.List_nth_default T) _ eq_refl); assumption
+                                   | eapply wf_update_annotation; wf_t
+                                   | wf_t
+                                   | match goal with
+                                     | [ H : context[UnderLets.wf _ _ _ _] |- UnderLets.wf _ _ _ _ ] => eapply H; solve [ repeat esplit; eauto ]
+                                     end
+                                   | eauto using List.nth_error_In
+                                   | eapply expr.wf_Proper_list; [ | eassumption ]; wf_safe_t; eauto 10 ]
+                           | break_innermost_match_step
+                           | match goal with
+                             | [ H : context[List.In] |- expr.wf _ ?x ?y ]
+                               => specialize (H x y); rewrite !List.nth_default_eq, <- List.combine_nth, <- !List.nth_default_eq in H; cbv [List.nth_default] in H |- *
+                             | [ H : List.In _ _ -> ?P |- ?P ] => apply H
+                             end
+                           | break_innermost_match_hyps_step
+                           | congruence
+                           | rewrite List.combine_length in *
+                           | rewrite NPeano.Nat.min_r in * by lia
+                           | rewrite NPeano.Nat.min_l in * by lia
+                           | progress expr.inversion_wf_one_constr
+                           | progress expr.invert_match ]. }
+          Qed.
+
+          Lemma wf_interp_ident_not_nth_default G {t} (idc : ident t)
+            : wf_value_with_lets G (Base (reflect1 (###idc)%expr (abstract_interp_ident _ idc))) (Base (reflect2 (###idc)%expr (abstract_interp_ident _ idc))).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper.
+            constructor; eapply wf_reflect;
+              solve [ apply bottom'_Proper
+                    | apply wf_annotate
+                    | repeat constructor
+                    | apply abstract_interp_ident_Proper; reflexivity ].
+          Qed.
+
+          Lemma wf_interp_ident G {t} idc1 idc2 (Hidc : idc1 = idc2)
+            : wf_value_with_lets G (@interp_ident1 t idc1) (@interp_ident2 t idc2).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper.
+            cbv [wf_value_with_lets ident.interp_ident]; subst idc2; destruct idc1;
+              first [ apply wf_interp_ident_nth_default
+                    | apply wf_interp_ident_not_nth_default ].
+          Qed.
+
+          Local Notation eval_with_bound1 := (@partial.ident.eval_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
+          Local Notation eval_with_bound2 := (@partial.ident.eval_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
+          Lemma wf_eval_with_bound {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
+                (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
+            : expr.wf G' (@eval_with_bound1 t e1 st1) (@eval_with_bound2 t e2 st2).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper.
+            eapply wf_eval_with_bound';
+              solve [ eassumption
+                    | eapply wf_annotate
+                    | eapply wf_interp_ident ].
+          Qed.
+
+          Local Notation eval1 := (@partial.ident.eval var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
+          Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
+          Lemma wf_eval {t} G G' e1 e2 (Hwf : expr.wf G e1 e2)
+                (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
+            : expr.wf G' (@eval1 t e1) (@eval2 t e2).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper.
+            eapply wf_eval';
+              solve [ eassumption
+                    | eapply wf_annotate
+                    | eapply wf_interp_ident ].
+          Qed.
+
+          Local Notation eta_expand_with_bound1 := (@partial.ident.eta_expand_with_bound var1 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
+          Local Notation eta_expand_with_bound2 := (@partial.ident.eta_expand_with_bound var2 abstract_domain' annotate_ident bottom' abstract_interp_ident update_literal_with_state extract_list_state is_annotation).
+          Lemma wf_eta_expand_with_bound {t} G e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
+            : expr.wf G (@eta_expand_with_bound1 t e1 st1) (@eta_expand_with_bound2 t e2 st2).
+          Proof using abstract_interp_ident_Proper annotate_ident_Proper bottom'_Proper extract_list_state_length extract_list_state_rel update_literal_with_state_Proper.
+            eapply wf_eta_expand_with_bound';
+              solve [ eassumption
+                    | eapply wf_annotate
+                    | eapply wf_interp_ident ].
+          Qed.
+        End with_var2.
+      End with_type.
+    End ident.
+
+    Section specialized.
+      Import defaults.
+      Local Notation abstract_domain' := ZRange.type.base.option.interp (only parsing).
+      Local Notation abstract_domain := (@partial.abstract_domain base.type abstract_domain').
+      Local Notation abstract_domain'_R t := (@eq (abstract_domain' t)) (only parsing).
+      Local Notation abstract_domain_R := (@abstract_domain_R base.type abstract_domain' (fun t => abstract_domain'_R t)).
+
+      Global Instance annotate_ident_Proper {t} : Proper (abstract_domain'_R t ==> eq) (annotate_ident t).
+      Proof.
+        intros st st' ?; subst st'.
+        cbv [annotate_ident]; break_innermost_match; reflexivity.
+      Qed.
+
+      Global Instance bottom'_Proper {t} : Proper (abstract_domain'_R t) (bottom' t).
+      Proof. reflexivity. Qed.
+
+      Global Instance abstract_interp_ident_Proper {t}
+        : Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t).
+      Proof.
+        cbv [abstract_interp_ident abstract_domain_R type.related respectful type.interp]; intros idc idc' ?; subst idc'; destruct idc;
+          repeat first [ reflexivity
+                       | progress subst
+                       | progress cbn [ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp Option.bind] in *
+                       | progress cbv [Option.bind]
+                       | intro
+                       | progress destruct_head'_prod
+                       | progress destruct_head'_bool
+                       | progress destruct_head' option
+                       | solve [ eauto ]
+                       | apply NatUtil.nat_rect_Proper_nondep
+                       | apply ListUtil.list_rect_Proper
+                       | apply ListUtil.list_case_Proper
+                       | apply ListUtil.pointwise_map
+                       | apply ListUtil.fold_right_Proper
+                       | apply ListUtil.update_nth_Proper
+                       | apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature)
+                       | cbn; apply (f_equal (@Some _))
+                       | match goal with
+                         | [ H : _ |- _ ] => erewrite H by (eauto; (eassumption || reflexivity))
+                         end ].
+      Qed.
+
+      Global Instance update_literal_with_state_Proper {t}
+        : Proper (abstract_domain'_R (base.type.type_base t) ==> eq ==> eq) (update_literal_with_state t).
+      Proof. repeat intro; congruence. Qed.
+
+      Global Instance extract_list_state_Proper {t}
+        : Proper (abstract_domain'_R _ ==> option_eq (SetoidList.eqlistA (@abstract_domain'_R t)))
+                 (extract_list_state t).
+      Proof.
+        intros st st' ?; subst st'; cbv [option_eq extract_list_state]; break_innermost_match; reflexivity.
+      Qed.
+
+      Lemma extract_list_state_length
+        : forall t v1 v2, abstract_domain'_R _ v1 v2 -> option_map (@length _) (extract_list_state t v1) = option_map (@length _) (extract_list_state t v2).
+      Proof.
+        intros; subst; cbv [option_map extract_list_state]; break_innermost_match; reflexivity.
+      Qed.
+      Lemma extract_list_state_rel
+        : forall t v1 v2, abstract_domain'_R _ v1 v2 -> forall l1 l2, extract_list_state t v1 = Some l1 -> extract_list_state t v2 = Some l2 -> forall vv1 vv2, List.In (vv1, vv2) (List.combine l1 l2) -> @abstract_domain'_R t vv1 vv2.
+      Proof.
+        intros; cbv [extract_list_state] in *; subst; inversion_option; subst.
+        rewrite combine_same, List.in_map_iff in *.
+        destruct_head'_ex; destruct_head'_and; inversion_prod; subst; reflexivity.
+      Qed.
+
+      Section with_var2.
+        Context {var1 var2 : type -> Type}.
+        Local Notation wf_value_with_lets := (@wf_value_with_lets base.type ident abstract_domain' (fun t => abstract_domain'_R t) var1 var2).
+
+        Lemma wf_eval {t} G G' e1 e2 (Hwf : expr.wf G e1 e2)
+              (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
+          : expr.wf G' (@eval var1 t e1) (@eval var2 t e2).
+        Proof.
+          eapply ident.wf_eval;
+            solve [ eassumption
+                  | exact _
+                  | apply extract_list_state_length
+                  | apply extract_list_state_rel ].
+        Qed.
+
+        Lemma wf_eval_with_bound {t} G G' e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
+              (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> wf_value_with_lets G' v1 v2)
+          : expr.wf G' (@eval_with_bound var1 t e1 st1) (@eval_with_bound var2 t e2 st2).
+        Proof.
+          eapply ident.wf_eval_with_bound;
+            solve [ eassumption
+                  | exact _
+                  | apply extract_list_state_length
+                  | apply extract_list_state_rel ].
+        Qed.
+
+
+        Lemma wf_eta_expand_with_bound {t} G e1 e2 (Hwf : expr.wf G e1 e2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
+          : expr.wf G (@eta_expand_with_bound var1 t e1 st1) (@eta_expand_with_bound var2 t e2 st2).
+        Proof.
+          eapply ident.wf_eta_expand_with_bound;
+            solve [ eassumption
+                  | exact _
+                  | apply extract_list_state_length
+                  | apply extract_list_state_rel ].
+        Qed.
+      End with_var2.
+
+      Lemma Wf_Eval {t} (e : Expr t) (Hwf : Wf e) : Wf (Eval e).
+      Proof.
+        intros ??; eapply wf_eval with (G:=nil); cbn [List.In]; try apply Hwf; tauto.
+      Qed.
+
+      Lemma Wf_EvalWithBound {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound)
+        : Wf (EvalWithBound e bound).
+      Proof.
+        intros ??; eapply wf_eval_with_bound with (G:=nil); cbn [List.In]; try apply Hwf; tauto.
+      Qed.
+
+      Lemma Wf_EtaExpandWithBound {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound)
+        : Wf (EtaExpandWithBound e bound).
+      Proof.
+        intros ??; eapply wf_eta_expand_with_bound with (G:=nil); cbn [List.In]; try apply Hwf; tauto.
+      Qed.
+
+      Local Instance Proper_strip_ranges {t}
+        : Proper (@abstract_domain_R t ==> @abstract_domain_R t) (@ZRange.type.option.strip_ranges t).
+      Proof.
+        cbv [Proper abstract_domain_R respectful].
+        induction t as [t|s IHs d IHd]; cbn in *; destruct_head'_prod; destruct_head'_and; cbn in *; intros; subst; cbv [respectful] in *;
+          eauto.
+      Qed.
+
+      Lemma Wf_EtaExpandWithListInfoFromBound {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound)
+        : Wf (EtaExpandWithListInfoFromBound e bound).
+      Proof.
+        eapply Wf_EtaExpandWithBound; [ assumption | ].
+        clear dependent e.
+        cbv [Proper] in *; induction t as [t|s IHs d IHd]; cbn in *; destruct_head'_prod; destruct_head'_and; cbn in *; eauto.
+        split; auto; apply Proper_strip_ranges; auto.
+      Qed.
+    End specialized.
+  End partial.
+  Import defaults.
+
+  Module RelaxZRange.
+    Module expr.
+      Section relax.
+        Context (relax_zrange : zrange -> option zrange)
+                (Hrelax : forall r r' z, is_tighter_than_bool z r = true
+                                         -> relax_zrange r = Some r'
+                                         -> is_tighter_than_bool z r' = true).
+        Section with_var2.
+          Context {var1 var2 : type -> Type}.
+
+          Lemma wf_relax G {t} (e1 : @expr var1 t) (e2 : @expr var2 t)
+                (Hwf : expr.wf G e1 e2)
+            : expr.wf G (@RelaxZRange.expr.relax relax_zrange var1 t e1) (@RelaxZRange.expr.relax relax_zrange var2 t e2).
+          Proof using Type.
+            clear -Hwf.
+            induction Hwf; wf_safe_t.
+            cbn [RelaxZRange.expr.relax]; cbv [option_map] in *.
+            break_innermost_match;
+              repeat first [ progress wf_safe_t
+                           | progress expr.invert_subst
+                           | progress expr.inversion_wf_constr
+                           | progress destruct_head' False
+                           | progress inversion_option
+                           | progress cbn [invert_Ident invert_Var invert_Abs invert_App invert_LetIn] in *
+                           | match goal with
+                             | [ H : context[RelaxZRange.expr.relax ?r ?x], H' : RelaxZRange.expr.relax ?r ?x = _ |- _ ]
+                               => rewrite H' in H
+                             | [ H : context[match RelaxZRange.expr.relax ?r ?x with _ => _ end] |- _ ]
+                               => remember (RelaxZRange.expr.relax r x) in *; progress expr.invert_match
+                             | [ H : ?x = Some ?a, H' : context[?x] |- _ ] => rewrite H in H'
+                             | [ H : ?x = None, H' : context[?x] |- _ ] => rewrite H in H'
+                             end
+                           | progress expr.inversion_wf_one_constr ].
+          Qed.
+        End with_var2.
+
+        Lemma Wf_Relax {t} (e : Expr t) (Hwf : Wf e) : Wf (@RelaxZRange.expr.Relax relax_zrange t e).
+        Proof. intros ??; eapply wf_relax, Hwf. Qed.
+      End relax.
+    End expr.
+  End RelaxZRange.
+  Hint Resolve RelaxZRange.expr.Wf_Relax : wf.
+
+  Lemma Wf_PartialEvaluateWithListInfoFromBounds
+        {t} (E : Expr t)
+        (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
+        (Hwf : Wf E)
+        {b_in_Proper : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R base.type ZRange.type.base.option.interp (fun t0 : base.type => eq))) b_in}
+    : Wf (PartialEvaluateWithListInfoFromBounds E b_in).
+  Proof. apply Wf_EtaExpandWithListInfoFromBound; assumption. Qed.
+  Hint Resolve Wf_PartialEvaluateWithListInfoFromBounds : wf.
+
+  Lemma Wf_PartialEvaluateWithBounds
+        {t} (E : Expr t)
+        (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
+        (Hwf : Wf E)
+        {b_in_Proper : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R base.type ZRange.type.base.option.interp (fun t0 : base.type => eq))) b_in}
+    : Wf (PartialEvaluateWithBounds E b_in).
+  Proof. eapply partial.Wf_EvalWithBound; assumption. Qed.
+  Hint Resolve Wf_PartialEvaluateWithBounds : wf.
+
+  Hint Resolve Wf_EtaExpandWithBound Wf_PartialEvaluateWithListInfoFromBounds : wf.
+End Compilers.
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index 437855405..3b8f81ac6 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -52,6 +52,7 @@ Require Crypto.Experiments.NewPipeline.LanguageWf.
 Require Crypto.Experiments.NewPipeline.UnderLetsProofs.
 Require Crypto.Experiments.NewPipeline.MiscCompilerPassesProofs.
 Require Crypto.Experiments.NewPipeline.RewriterProofs.
+Require Crypto.Experiments.NewPipeline.AbstractInterpretationWf.
 Require Crypto.Experiments.NewPipeline.AbstractInterpretationProofs.
 Require Import Crypto.Util.Notations.
 Import ListNotations. Local Open Scope Z_scope.
@@ -499,6 +500,7 @@ Import
   Crypto.Experiments.NewPipeline.UnderLetsProofs
   Crypto.Experiments.NewPipeline.MiscCompilerPassesProofs
   Crypto.Experiments.NewPipeline.RewriterProofs
+  Crypto.Experiments.NewPipeline.AbstractInterpretationWf
   Crypto.Experiments.NewPipeline.AbstractInterpretationProofs
   Crypto.Experiments.NewPipeline.Language
   Crypto.Experiments.NewPipeline.UnderLets
@@ -512,6 +514,7 @@ Import
   UnderLetsProofs.Compilers
   MiscCompilerPassesProofs.Compilers
   RewriterProofs.Compilers
+  AbstractInterpretationWf.Compilers
   AbstractInterpretationProofs.Compilers
   Language.Compilers
   UnderLets.Compilers