diff --git a/src/AbstractInterpretation/AbstractInterpretation.v b/src/AbstractInterpretation/AbstractInterpretation.v
index c43ead4fc9..5345c0e3c3 100644
--- a/src/AbstractInterpretation/AbstractInterpretation.v
+++ b/src/AbstractInterpretation/AbstractInterpretation.v
@@ -34,7 +34,8 @@ Module Compilers.
               {var : type -> Type}.
       Local Notation expr := (@expr base_type ident).
       Local Notation UnderLets := (@UnderLets base_type ident var).
-      Context (abstract_domain' : base_type -> Type)
+      Context {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type}
+              (abstract_domain' : base_type -> Type)
               (annotate : forall (is_let_bound : bool) t, abstract_domain' t -> @expr var t -> UnderLets (@expr var t))
               (bottom' : forall A, abstract_domain' A)
               (skip_annotations_under : forall t, ident t -> bool).
@@ -42,18 +43,25 @@ Module Compilers.
       Definition abstract_domain (t : type)
         := type.interp abstract_domain' t.
 
-      Fixpoint value (t : type)
+      Context {default_expr : @DefaultValue.type.base.DefaultT _ (@expr abstract_domain)}. (* needed for impossible cases *)
+
+      (** A value should carry both an abstract state and a way of turning value's into expressions *)
+      Fixpoint value' (t : type)
         := match t return Type (* COQBUG(https://github.com/coq/coq/issues/7727) *) with
            | type.base t
-             => abstract_domain t * @expr var t
+             => @expr var t
            | type.arrow s d
-             => value s -> UnderLets (value d)
+             => abstract_domain s * value' s -> UnderLets (value' d)
            end%type.
 
-      Definition value_with_lets (t : type)
-        := UnderLets (value t).
+      Definition value (t : type) : Type
+        := abstract_domain t * UnderLets (value' t).
+
+      Context (ident_extract : forall t, ident t -> abstract_domain t).
+      Context (interp_ident' : bool (* annotate with state? *) -> forall t, ident t -> UnderLets (value' t)).
 
-      Context (interp_ident : bool (* annotate with state? *) -> forall t, ident t -> value_with_lets t).
+      Definition interp_ident (annotate_with_state : bool) {t} (idc : ident t) : value t
+        := (ident_extract _ idc, interp_ident' annotate_with_state _ idc).
 
       Fixpoint bottom {t} : abstract_domain t
         := match t with
@@ -67,54 +75,50 @@ Module Compilers.
            | type.arrow s d => (bottom, @bottom_for_each_lhs_of_arrow d)
            end.
 
-      Definition state_of_value {t} : value t -> abstract_domain t
-        := match t return value t -> abstract_domain t with
-           | type.base t => fun '(st, v) => st
-           | type.arrow s d => fun _ => bottom
-           end.
+      Definition state_of_value {t} : value t -> abstract_domain t := fst.
+      Definition project_value' {t} : value t -> UnderLets (value' t) := snd.
+      Definition Base_value' {t} : abstract_domain t * value' t -> value t
+        := fun x => (fst x, Base (snd x)).
+      Definition apply_value {s d} (f : value (s -> d)) (x : value s) : value d
+        := let '(x1, x2) := (state_of_value x, project_value' x) in
+           let '(f1, f2) := (state_of_value f, project_value' f) in
+           (f1 x1, (f2 <-- f2; x2 <-- x2; f2 (x1, x2))%under_lets).
 
-      (** We need to make sure that we ignore the state of
-         higher-order arrows *everywhere*, or else the proofs don't go
-         through.  So we sometimes need to replace the state of
-         arrow-typed values with [⊥]. *)
-      Fixpoint bottomify {t} : value t -> value_with_lets t
-        := match t return value t -> value_with_lets t with
-           | type.base t => fun '(st, v) => Base (bottom' t, v)
-           | type.arrow s d => fun f => Base (fun x => fx <-- f x; @bottomify d fx)
-           end%under_lets.
-
-      (** We drop the state of higher-order arrows *)
       Fixpoint reify (annotate_with_state : bool) (is_let_bound : bool) {t} : value t -> type.for_each_lhs_of_arrow abstract_domain t -> UnderLets (@expr var t)
         := match t return value t -> type.for_each_lhs_of_arrow abstract_domain t -> UnderLets (@expr var t) with
            | type.base t
              => fun '(st, v) 'tt
-                => if annotate_with_state
-                   then annotate is_let_bound t st v
-                   else if is_let_bound
-                        then UnderLets.UnderLet v (fun v' => UnderLets.Base ($$v'))
-                        else UnderLets.Base v
+                => (v <-- v;
+                    if annotate_with_state
+                    then annotate is_let_bound t st v
+                    else if is_let_bound
+                         then UnderLets.UnderLet v (fun v' => UnderLets.Base ($$v'))
+                         else UnderLets.Base v)
            | type.arrow s d
              => fun f_e '(sv, dv)
-               => let sv := match s with
-                           | type.base _ => sv
-                           | type.arrow _ _ => bottom
-                           end in
-                 Base
-                   (λ x , (UnderLets.to_expr
-                             (fx <-- f_e (@reflect annotate_with_state _ (expr.Var x) sv);
-                                @reify annotate_with_state false _ fx dv)))
-           end%core%expr
+                => (let f := state_of_value f_e in
+                    f_e <-- project_value' f_e;
+                    Base
+                      (λ x , UnderLets.to_expr
+                               (let sv := @reflect annotate_with_state _ (expr.Var x) sv in
+                                let sx := state_of_value sv in
+                                x <-- project_value' sv;
+                                fx <-- f_e (sx, x)%core;
+                                @reify annotate_with_state false _ (f sx, Base fx)%core dv)))
+           end%core%expr%under_lets
       with reflect (annotate_with_state : bool) {t} : @expr var t -> abstract_domain t -> value t
            := match t return @expr var t -> abstract_domain t -> value t with
               | type.base t
-                => fun e st => (st, e)
+                => fun e st => Base_value' (st, e)
               | type.arrow s d
                 => fun e absf
-                   => (fun v
-                       => let stv := state_of_value v in
-                          (rv <-- (@reify annotate_with_state false s v bottom_for_each_lhs_of_arrow);
-                             Base (@reflect annotate_with_state d (e @ rv) (absf stv))%expr))
-              end%under_lets.
+                   => Base_value'
+                        (absf,
+                          (fun v
+                           => rv <-- @reify annotate_with_state false s (Base_value' v) bottom_for_each_lhs_of_arrow;
+                           (* TODO: Should we be feeding in [fst v], or should we bottom out the arguments to [fst v]? *)
+                           project_value' (@reflect annotate_with_state d (e @ rv) (absf (fst v)))%expr))
+              end%under_lets%core.
 
       Definition skip_annotations_for_App {var'} {t} (e : @expr var' t) : bool
         := match invert_AppIdent_curried e with
@@ -122,64 +126,74 @@ Module Compilers.
            | None => false
            end.
 
-      Fixpoint interp (annotate_with_state : bool) {t} (e : @expr value_with_lets t) : value_with_lets t
+      Definition invert_default {A B} (t : type) (x : option { t : type & @expr abstract_domain (A t) * @expr abstract_domain (B t) }%type) : @expr abstract_domain (A t) * @expr abstract_domain (B t)
+        := Option.value
+             (type.try_transport
+                _ _ t
+                (projT2
+                   (Option.value x (existT _ t (DefaultValue.type.base.defaultv, DefaultValue.type.base.defaultv)))))
+             (DefaultValue.type.base.defaultv, DefaultValue.type.base.defaultv).
+
+      Definition invert_default' {A B C} (t : type) (x : option { t : type & @expr abstract_domain (A t) * (abstract_domain (B t) -> @expr abstract_domain (C t)) }%type) : @expr abstract_domain (A t) * (abstract_domain (B t) -> @expr abstract_domain (C t))
+        := Option.value
+             (type.try_transport
+                _ _ t
+                (projT2
+                   (Option.value x (existT _ t (DefaultValue.type.base.defaultv, fun _ => DefaultValue.type.base.defaultv)))))
+             (DefaultValue.type.base.defaultv, fun _ => DefaultValue.type.base.defaultv).
+
+      Fixpoint interp (annotate_with_state : bool) {t} (e : @expr value t) : @expr abstract_domain t -> value t
         := let annotate_with_state := annotate_with_state && negb (skip_annotations_for_App e) in
-           match e in expr.expr t return value_with_lets t with
-           | expr.Ident t idc => interp_ident annotate_with_state _ idc (* Base (reflect (###idc) (abstract_interp_ident _ idc))*)
-           | expr.Var t v => v
-           | expr.Abs s d f => Base (fun x => @interp annotate_with_state d (f (Base x)))
-           | expr.App (type.base s) d f x
-             => (x' <-- @interp annotate_with_state _ x;
-                   f' <-- @interp annotate_with_state (_ -> d)%etype f;
-                   f' x')
-           | expr.App (type.arrow s' d') d f x
-             => (x' <-- @interp annotate_with_state (s' -> d')%etype x;
-                   x'' <-- bottomify x';
-                   f' <-- @interp annotate_with_state (_ -> d)%etype f;
-                   f' x'')
-           | expr.LetIn (type.arrow _ _) B x f
-             => (x' <-- @interp annotate_with_state _ x;
-                   @interp annotate_with_state _ (f (Base x')))
-           | expr.LetIn (type.base A) B x f
-             => (x' <-- @interp annotate_with_state _ x;
-                   x'' <-- reify annotate_with_state true (* this forces a let-binder here *) x' tt;
-                   @interp annotate_with_state _ (f (Base (reflect annotate_with_state x'' (state_of_value x')))))
+           let expr_interp {t} := expr.interp (@ident_extract) (t:=t) in
+           match e in expr.expr t return @expr abstract_domain t -> value t with
+           | expr.Ident t idc => fun _ => @interp_ident annotate_with_state _ idc (* Base (reflect (###idc) (abstract_interp_ident _ idc))*)
+           | expr.Var t v => fun _ => v
+           | expr.Abs s d f
+             => fun fe_st
+                => let f_st := expr_interp fe_st in
+                   let fe_st := Option.value (invert_Abs fe_st) ((* should never happen *)fun _ => DefaultValue.type.base.defaultv) in
+                   Base_value'
+                     (f_st,
+                       (fun x
+                        => project_value' (@interp annotate_with_state d (f (Base_value' x)) (fe_st (fst x)))))
+           | expr.App s d f x
+             => fun fx_st
+                => (let '(f_st, x_st) := invert_default s (invert_App fx_st) in
+                    let x := @interp annotate_with_state s x x_st in
+                    let f := @interp annotate_with_state (s -> d)%etype f f_st in
+                    apply_value f x)
+           | expr.LetIn (type.base A' as A) B x f
+             => fun st
+                => let '(x_st, f_st) := invert_default' A (invert_LetIn st) in
+                   let x := @interp annotate_with_state _ x x_st in
+                   let x_st := state_of_value x in
+                   let fx_st := f_st x_st in
+                   (expr_interp fx_st,
+                     x <-- reify annotate_with_state true (* this forces a let-binder here *) x tt;
+                    project_value' (@interp annotate_with_state _ (f (reflect annotate_with_state x x_st)) fx_st))
+           | expr.LetIn (type.arrow _ _ as A) B x f
+             => fun st
+                => let '(x_st, f_st) := invert_default' A (invert_LetIn st) in
+                   let x := @interp annotate_with_state _ x x_st in
+                   @interp annotate_with_state _ (f x) (f_st (state_of_value x))
            end%under_lets.
 
-      Definition eval_with_bound' (annotate_with_state : bool) {t} (e : @expr value_with_lets t)
+      Definition eval_with_bound' (annotate_with_state : bool) {t} (e : @expr value t) (e_st : @expr abstract_domain t)
                  (st : type.for_each_lhs_of_arrow abstract_domain t)
         : expr t
-        := UnderLets.to_expr (e' <-- interp annotate_with_state e; reify annotate_with_state false e' st).
+        := UnderLets.to_expr (reify annotate_with_state false (interp annotate_with_state e e_st) st).
 
-      Definition eval' {t} (e : @expr value_with_lets t) : expr t
-        := eval_with_bound' false e bottom_for_each_lhs_of_arrow.
+      Definition eval' {t} (e : @expr value t) (e_st : @expr abstract_domain t) : expr t
+        := eval_with_bound' false e e_st bottom_for_each_lhs_of_arrow.
 
       Definition eta_expand_with_bound' {t} (e : @expr var t)
                  (st : type.for_each_lhs_of_arrow abstract_domain t)
         : expr t
         := UnderLets.to_expr (reify true false (reflect true e bottom) st).
 
-      Section extract.
-        Context (ident_extract : forall t, ident t -> abstract_domain t).
-
-        (** like [expr.interp (@ident_extract) e], except we replace
-            all higher-order state with bottom *)
-        Fixpoint extract' {t} (e : @expr abstract_domain t) : abstract_domain t
-          := match e in expr.expr t return abstract_domain t with
-             | expr.Ident t idc => ident_extract t idc
-             | expr.Var t v => v
-             | expr.Abs s d f => fun v : abstract_domain s => @extract' _ (f v)
-             | expr.App (type.base s) d f x
-               => @extract' _ f (@extract' _ x)
-             | expr.App (type.arrow s' d') d f x
-               => @extract' _ f (@bottom (type.arrow s' d'))
-             | expr.LetIn A B x f => dlet y := @extract' _ x in @extract' _ (f y)
-             end.
-
-        Definition extract_gen {t} (e : @expr abstract_domain t) (bound : type.for_each_lhs_of_arrow abstract_domain t)
-          : abstract_domain' (type.final_codomain t)
-          := type.app_curried (extract' e) bound.
-      End extract.
+      Definition extract_gen {t} (e : @expr abstract_domain t) (bound : type.for_each_lhs_of_arrow abstract_domain t)
+        : abstract_domain' (type.final_codomain t)
+        := type.app_curried (expr.interp (@ident_extract) e) bound.
     End with_var.
 
     Module ident.
@@ -194,8 +208,8 @@ Module Compilers.
         Local Notation UnderLets := (@UnderLets base.type ident var).
         Context (abstract_domain' : base.type -> Type).
         Local Notation abstract_domain := (@abstract_domain base.type abstract_domain').
-        Local Notation value_with_lets := (@value_with_lets base.type ident var abstract_domain').
         Local Notation value := (@value base.type ident var abstract_domain').
+        Local Notation value' := (@value' base.type ident var abstract_domain').
         Context (annotate_expr : forall t, abstract_domain' t -> option (@expr var (t -> t)))
                 (bottom' : forall A, abstract_domain' A)
                 (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t)
@@ -204,7 +218,7 @@ Module Compilers.
                 (is_annotated_for : forall t t', @expr var t -> abstract_domain' t' -> bool)
                 (annotation_to_cast : forall s d, @expr var (s -> d) -> option (@expr var s -> @expr var d))
                 (skip_annotations_under : forall t, ident t -> bool)
-                (strip_annotation : forall t, ident t -> option (value t)).
+                (strip_annotation : forall t, ident t -> option (value' t)).
 
         (** TODO: Is it okay to commute annotations? *)
         Definition update_annotation {t} (st : abstract_domain' t) (e : @expr var t) : @expr var t
@@ -286,34 +300,35 @@ Module Compilers.
 
         Local Notation reify := (@reify base.type ident var abstract_domain' annotate bottom').
         Local Notation reflect := (@reflect base.type ident var abstract_domain' annotate bottom').
+        Local Notation apply_value := (@apply_value base.type ident var abstract_domain').
+        Local Notation Base_value' := (@Base_value' base.type ident var abstract_domain').
 
         (** We manually rewrite with the rule for [nth_default], as the eliminator for eta-expanding lists in the input *)
-        Definition interp_ident (annotate_with_state : bool) {t} (idc : ident t) : value_with_lets t
-          := match idc in ident t return value_with_lets t with
+        Definition interp_ident' (annotate_with_state : bool) {t} (idc : ident t) : UnderLets (value' t)
+          := match idc in ident t return UnderLets (value' t) with
              | ident.List_nth_default T as idc
-               => let default := reflect annotate_with_state (###idc) (abstract_interp_ident _ idc) in
-                  Base
-                    (fun default_arg
-                     => default <-- default default_arg;
-                          Base
-                            (fun ls_arg
-                             => default <-- default ls_arg;
-                                  Base
-                                    (fun n_arg
-                                     => default <-- default n_arg;
-                                          ls' <-- @reify annotate_with_state false (base.type.list T) ls_arg tt;
-                                          Base
-                                            (fst default,
-                                             match reflect_list ls', invert_Literal (snd n_arg) with
-                                             | Some ls, Some n
-                                               => nth_default (snd default_arg) ls n
-                                             | _, _ => snd default
-                                             end))))
-             | idc => Base
-                        match strip_annotation _ idc with
-                        | Some v => v
-                        | None => reflect annotate_with_state (###idc) (abstract_interp_ident _ idc)
-                        end
+               => let '(default_st, default) := reflect annotate_with_state (###idc) (abstract_interp_ident _ idc) in
+                  (default <-- default;
+                   Base
+                     (fun default_arg
+                      => default <-- default default_arg;
+                      Base
+                        (fun ls_arg
+                         => default <-- default ls_arg;
+                         Base
+                           (fun n_arg
+                            => default <-- default n_arg;
+                            ls' <-- @reify annotate_with_state false (base.type.list T) (Base_value' ls_arg) tt;
+                            Base
+                              match reflect_list ls', invert_Literal (snd n_arg) with
+                              | Some ls, Some n
+                                => nth_default (snd default_arg) ls n
+                              | _, _ => default
+                              end))))
+             | idc => match strip_annotation _ idc with
+                      | Some v => Base v
+                      | None => project_value' _ (reflect annotate_with_state (###idc) (abstract_interp_ident _ idc))
+                      end
              end%core%under_lets%expr.
 
         Fixpoint strip_all_annotations' (should_strip : bool) {t} (e : @expr var t) : @expr var t
@@ -343,13 +358,13 @@ Module Compilers.
         Definition strip_all_annotations {t} (e : @expr var t) : @expr var t
           := @strip_all_annotations' false t e.
 
-        Definition eval_with_bound (skip_annotations_under : forall t, ident t -> bool) (annotate_with_state : bool) {t} (e : @expr value_with_lets t)
+        Definition eval_with_bound (skip_annotations_under : forall t, ident t -> bool) (annotate_with_state : bool) {t} (e : @expr value t) (e_st : @expr abstract_domain t)
                    (st : type.for_each_lhs_of_arrow abstract_domain t)
           : @expr var t
-          := @eval_with_bound' base.type ident var abstract_domain' annotate bottom' skip_annotations_under interp_ident annotate_with_state t e st.
+          := @eval_with_bound' base.type ident var _ abstract_domain' annotate bottom' skip_annotations_under _ abstract_interp_ident interp_ident' annotate_with_state t e e_st st.
 
-        Definition eval {t} (e : @expr value_with_lets t) : @expr var t
-          := @eval' base.type ident var abstract_domain' annotate bottom' (fun _ _ => false) interp_ident t e.
+        Definition eval {t} (e : @expr value t) (e_st : @expr abstract_domain t) : @expr var t
+          := @eval' base.type ident var _ abstract_domain' annotate bottom' (fun _ _ => false) _ abstract_interp_ident interp_ident' t e e_st.
 
         Definition eta_expand_with_bound {t} (e : @expr var t)
                    (st : type.for_each_lhs_of_arrow abstract_domain t)
@@ -357,7 +372,7 @@ Module Compilers.
           := @eta_expand_with_bound' base.type ident var abstract_domain' annotate bottom' t e st.
 
         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' bottom' abstract_interp_ident t e bound.
+          := @extract_gen base.type ident abstract_domain' abstract_interp_ident t e bound.
       End with_var.
     End ident.
 
@@ -366,8 +381,8 @@ Module Compilers.
     Section specialized.
       Local Notation abstract_domain' := ZRange.type.base.option.interp.
       Local Notation abstract_domain := (@partial.abstract_domain base.type abstract_domain').
-      Local Notation value_with_lets var := (@value_with_lets base.type ident var abstract_domain').
       Local Notation value var := (@value base.type ident var abstract_domain').
+      Local Notation value' var := (@value' base.type ident var abstract_domain').
       Notation expr := (@expr base.type ident).
       Notation Expr := (@expr.Expr base.type ident).
       Local Notation type := (type base.type).
@@ -412,8 +427,8 @@ Module Compilers.
         Definition abstract_interp_ident {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) t (idc : ident t) : type.interp abstract_domain' t
           := ZRange.ident.option.interp assume_cast_truncates idc.
 
-        Definition always_strip_annotation {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {var} t (idc : ident t) : option (value var t)
-          := match idc in ident t return option (value var t) with
+        Definition always_strip_annotation {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {var} t (idc : ident t) : option (value' var t)
+          := match idc in ident t return option (value' var t) with
              | ident.Z_cast as idc
              | ident.Z_cast2 as idc
                => let tZ_type := (fun t (idc : ident (type.base _ -> type.base t -> type.base t)) => t) _ idc in (* we want Coq to pick up the Z type for bounds tightness, not the zrange type (where "tighter" means "equal") *)
@@ -422,8 +437,7 @@ Module Compilers.
                      => Base
                           (fun '(r_known, e)
                            => Base
-                                ((abstract_interp_ident assume_cast_truncates _ idc r_orig r_known,
-                                  let do_strip
+                                (let do_strip
                                       := match ZRange.type.base.option.lift_Some r_known, ZRange.type.base.option.lift_Some r_orig with
                                          | Some r_known, Some r_orig
                                            => ZRange.type.base.is_tighter_than
@@ -433,11 +447,11 @@ Module Compilers.
                                          end in
                                   if do_strip
                                   then e
-                                  else (###idc @ re @ e)%expr))))
+                                  else (###idc @ re @ e)%expr)))
              | _ => None
              end.
 
-        Definition strip_annotation {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (strip_annotations : bool) {var} : forall t, ident t -> option (value var t)
+        Definition strip_annotation {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (strip_annotations : bool) {var} : forall t, ident t -> option (value' var t)
           := if strip_annotations
              then always_strip_annotation assume_cast_truncates
              else fun _ _ => None.
@@ -485,10 +499,10 @@ Module Compilers.
         Definition strip_all_annotations strip_annotations_under {var} {t} (e : @expr var t) : @expr var t
           := @ident.strip_all_annotations var (@annotation_to_cast _) strip_annotations_under t e.
 
-        Definition eval_with_bound {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (skip_annotations_under : forall t, ident t -> bool) (strip_preexisting_annotations : bool) {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
+        Definition eval_with_bound {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (skip_annotations_under : forall t, ident t -> bool) (strip_preexisting_annotations : bool) {var} {t} (e e_st : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
           := let annotate_with_state := true in
              (@partial.ident.eval_with_bound)
-               var abstract_domain' annotate_expr bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state is_annotated_for (strip_annotation assume_cast_truncates strip_preexisting_annotations) skip_annotations_under annotate_with_state t e bound.
+               var abstract_domain' annotate_expr bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state is_annotated_for (strip_annotation assume_cast_truncates strip_preexisting_annotations) skip_annotations_under annotate_with_state t e e_st bound.
 
         Definition eta_expand_with_bound {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
           := let assume_cast_truncates := false in
@@ -499,35 +513,39 @@ Module Compilers.
         Definition StripAllAnnotations strip_annotations_under {t} (e : Expr t) : Expr t
           := fun var => strip_all_annotations strip_annotations_under (e _).
 
-        Definition EvalWithBound {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (skip_annotations_under : forall t, ident t -> bool) (strip_preexisting_annotations : bool) {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
-          := fun var => eval_with_bound assume_cast_truncates skip_annotations_under strip_preexisting_annotations (e _) bound.
+        Definition EvalWithBound {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (skip_annotations_under : forall t, ident t -> bool) (strip_preexisting_annotations : bool) {t} (E : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
+          := dlet_nd e := GeneralizeVar.ToFlat E in
+              let E := GeneralizeVar.FromFlat e in
+              fun var => eval_with_bound assume_cast_truncates skip_annotations_under strip_preexisting_annotations (E _) (E _) bound.
         Definition EtaExpandWithBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
           := fun var => eta_expand_with_bound (e _) bound.
       End with_relax.
 
-      Definition strip_annotations {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {var} {t} (e : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
+      Definition strip_annotations {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {var} {t} (e e_st : @expr _ t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : expr t
         := let strip_preexisting_annotations := true in
            let annotate_with_state := false in
            let skip_annotations_under := fun _ _ => false in
            (@partial.ident.eval_with_bound)
-             var abstract_domain' (annotate_expr default_relax_zrange) bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state (is_annotated_for default_relax_zrange) (strip_annotation assume_cast_truncates strip_preexisting_annotations) skip_annotations_under annotate_with_state t e bound.
+             var abstract_domain' (annotate_expr default_relax_zrange) bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state (is_annotated_for default_relax_zrange) (strip_annotation assume_cast_truncates strip_preexisting_annotations) skip_annotations_under annotate_with_state t e e_st bound.
 
       Definition StripAnnotations {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
-        := fun var => strip_annotations assume_cast_truncates (e _) bound.
+        := fun var => strip_annotations assume_cast_truncates (e _) (e _) bound.
 
-      Definition eval {opts : AbstractInterpretation.Options} {var} {t} (e : @expr _ t) : expr t
+      Definition eval {opts : AbstractInterpretation.Options} {var} {t} (e e_st : @expr _ t) : expr t
         := let assume_cast_truncates := false in
            let strip_preexisting_annotations := false in
            (@partial.ident.eval)
-             var abstract_domain' (annotate_expr default_relax_zrange) bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state (is_annotated_for default_relax_zrange) (strip_annotation assume_cast_truncates strip_preexisting_annotations)  t e.
-      Definition Eval {opts : AbstractInterpretation.Options} {t} (e : Expr t) : Expr t
-        := fun var => eval (e _).
+             var abstract_domain' (annotate_expr default_relax_zrange) bottom' (abstract_interp_ident assume_cast_truncates) extract_list_state extract_option_state (is_annotated_for default_relax_zrange) (strip_annotation assume_cast_truncates strip_preexisting_annotations) t e e_st.
+      Definition Eval {opts : AbstractInterpretation.Options} {t} (E : Expr t) : Expr t
+        := dlet_nd e := GeneralizeVar.ToFlat E in
+            let E := GeneralizeVar.FromFlat e in
+            fun var => eval (E _) (E _).
       Definition EtaExpandWithListInfoFromBound {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : Expr t
         := EtaExpandWithBound default_relax_zrange e (type.map_for_each_lhs_of_arrow (@ZRange.type.option.strip_ranges) bound).
       Definition extract {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {t} (e : expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t)
-        := @partial.ident.extract abstract_domain' bottom' (abstract_interp_ident assume_cast_truncates) t e bound.
+        := @partial.ident.extract abstract_domain' (abstract_interp_ident assume_cast_truncates) t e bound.
       Definition Extract {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {t} (e : Expr t) (bound : type.for_each_lhs_of_arrow abstract_domain t) : abstract_domain' (type.final_codomain t)
-        := @partial.ident.extract abstract_domain' bottom' (abstract_interp_ident assume_cast_truncates) t (e _) bound.
+        := @partial.ident.extract abstract_domain' (abstract_interp_ident assume_cast_truncates) t (e _) bound.
     End specialized.
   End partial.
   Import API.
diff --git a/src/AbstractInterpretation/Proofs.v b/src/AbstractInterpretation/Proofs.v
index 22a96f8bff..3be4a84e0d 100644
--- a/src/AbstractInterpretation/Proofs.v
+++ b/src/AbstractInterpretation/Proofs.v
@@ -3,6 +3,7 @@ Require Import Coq.ZArith.ZArith.
 Require Import Coq.Classes.Morphisms.
 Require Import Coq.Classes.RelationPairs.
 Require Import Coq.Relations.Relations.
+Require Import Crypto.Util.Bool.Reflect.
 Require Import Crypto.Util.ZRange.
 Require Import Crypto.Util.ZRange.Operations.
 Require Import Crypto.Util.ZRange.BasicLemmas.
@@ -100,80 +101,133 @@ Module Compilers.
               (bottom'_related : forall t v, abstraction_relation' t (bottom' t) v)
               (skip_annotations_under : forall t, ident t -> bool)
               (abstract_interp_ident : forall t, ident t -> type.interp abstract_domain' t)
-              (ident_interp_Proper : forall t (idc : ident t), type.related_hetero abstraction_relation' (abstract_interp_ident t idc) (ident_interp t idc))
+              (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop).
+      Local Notation abstract_domain := (@abstract_domain base_type abstract_domain').
+      Local Notation abstract_domain_R := (@abstract_domain_R base_type abstract_domain' abstract_domain'_R).
+      (* we only care about inputs that are extensional, so we restrict this here *)
+      (* skip_base:=true because abstract_domain'_R refl and eqv refl follows from abstraction_relation' *)
+      Definition abstraction_relation {t} : abstract_domain t -> type.interp base_interp t -> Prop
+        := type.related_hetero_and_Proper (skip_base:=true) (@abstract_domain'_R) (fun _ => eq) (@abstraction_relation').
+      (*Definition abstraction_relation {t} : abstract_domain t -> type.interp base_interp t -> Prop
+        := type.related_hetero (@abstraction_relation').*)
+      Context (ident_interp_Proper : forall t (idc : ident t), abstraction_relation (abstract_interp_ident t idc) (ident_interp t idc))
               (ident_interp_Proper' : forall t, Proper (eq ==> type.eqv) (ident_interp t))
-              (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop)
               (abstraction_relation'_Proper : forall t, Proper (abstract_domain'_R t ==> eq ==> Basics.impl) (abstraction_relation' t))
               {abstract_domain'_R_transitive : forall t, Transitive (@abstract_domain'_R t)}
               {abstract_domain'_R_symmetric : forall t, Symmetric (@abstract_domain'_R t)}
               {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)}
+              (base_type_beq : base_type -> base_type -> bool)
+              {reflect_base_type_beq : reflect_rel eq base_type_beq}
+              {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type}
+              {try_make_transport_base_type_cps_correct : type.try_make_transport_cps_correctT base_type}
               (abstract_domain'_R_of_related : forall t st v, @abstraction_relation' t st v -> @abstract_domain'_R t st st).
-      Local Notation abstract_domain := (@abstract_domain base_type abstract_domain').
-      Definition abstraction_relation {t} : abstract_domain t -> type.interp base_interp t -> Prop
-        := type.related_hetero (@abstraction_relation').
       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')).
-      Local Notation abstract_domain_R := (@abstract_domain_R base_type abstract_domain' abstract_domain'_R).
       Local Notation var := (type.interp base_interp).
       Local Notation expr := (@expr.expr base_type ident).
       Local Notation UnderLets := (@UnderLets base_type ident).
+      Local Notation value' := (@value' base_type ident var abstract_domain').
       Local Notation value := (@value base_type ident var abstract_domain').
-      Local Notation value_with_lets := (@value_with_lets base_type ident var abstract_domain').
-      Local Notation state_of_value := (@state_of_value base_type ident var abstract_domain' bottom').
+      Local Notation state_of_value := (@state_of_value base_type ident var abstract_domain').
+      Local Notation project_value' := (@project_value' base_type ident var abstract_domain').
+      Local Notation extract_gen := (@extract_gen base_type ident abstract_domain' abstract_interp_ident).
+      Context {default_expr : @DefaultValue.type.base.DefaultT _ (@expr abstract_domain)}. (* needed for impossible cases *)
       Context (annotate : forall (is_let_bound : bool) t, abstract_domain' t -> @expr var t -> @UnderLets var (@expr var t))
-              (interp_ident : bool -> forall t, ident t -> value_with_lets t)
-              (ident_extract : forall t, ident t -> abstract_domain t)
+              (interp_ident' : bool -> forall t, ident t -> @UnderLets var (value' t))
               (interp_annotate
                : forall is_let_bound t st e
                    (He : abstraction_relation' t st (expr.interp (t:=type.base t) (@ident_interp) e)),
                   expr.interp (@ident_interp) (UnderLets.interp (@ident_interp) (@annotate is_let_bound t st e))
                   = expr.interp (@ident_interp) e)
-              (ident_extract_Proper : forall t, Proper (eq ==> abstract_domain_R) (ident_extract t)).
+              (abstract_interp_ident_Proper : forall t, Proper (eq ==> abstract_domain_R) (abstract_interp_ident t)).
       Local Notation eta_expand_with_bound' := (@eta_expand_with_bound' base_type ident _ abstract_domain' annotate bottom').
-      Local Notation eval_with_bound' := (@partial.eval_with_bound' base_type ident _ abstract_domain' annotate bottom' skip_annotations_under interp_ident).
-      Local Notation extract' := (@extract' base_type ident abstract_domain' bottom' ident_extract).
-      Local Notation extract_gen := (@extract_gen base_type ident abstract_domain' bottom' ident_extract).
+      Local Notation eval_with_bound' := (@partial.eval_with_bound' base_type ident _ try_make_transport_base_type_cps abstract_domain' annotate bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident').
       Local Notation reify := (@reify base_type ident _ abstract_domain' annotate bottom').
       Local Notation reflect := (@reflect base_type ident _ abstract_domain' annotate bottom').
-      Local Notation interp := (@interp base_type ident var abstract_domain' annotate bottom' skip_annotations_under interp_ident).
-      Local Notation bottomify := (@bottomify base_type ident _ abstract_domain' bottom').
-
-      Lemma bottom_related t v : @abstraction_relation t bottom v.
-      Proof using bottom'_related. cbv [abstraction_relation]; induction t; cbn; cbv [respectful_hetero]; eauto. Qed.
-
-      Local Hint Resolve bottom_related : core typeclass_instances.
+      Local Notation interp := (@interp base_type ident var try_make_transport_base_type_cps abstract_domain' annotate bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident').
+      Local Notation invert_default := (@invert_default base_type ident try_make_transport_base_type_cps abstract_domain' default_expr).
+      Local Notation invert_default' := (@invert_default' base_type ident try_make_transport_base_type_cps abstract_domain' default_expr).
+      Local Notation interp_ident := (@interp_ident base_type ident var abstract_domain' abstract_interp_ident interp_ident').
+
+      Lemma abstract_domain_R_refl_of_abstraction_relation {t st v}
+        : @abstraction_relation t st v -> Proper abstract_domain_R st.
+      Proof using abstract_domain'_R_of_related. apply type.related_hetero_and_Proper_proj1, abstract_domain'_R_of_related. Qed.
+      Local Hint Immediate abstract_domain_R_refl_of_abstraction_relation : core typeclass_instances.
+      Lemma eqv_refl_of_abstraction_relation {t st v}
+        : @abstraction_relation t st v -> v == v.
+      Proof using Type. apply type.related_hetero_and_Proper_proj2; repeat intro; hnf; auto. Qed.
+      Local Hint Immediate eqv_refl_of_abstraction_relation : core typeclass_instances.
+
+      Lemma eqv_refl_of_abstraction_relation_for_each_lhs_of_arrow {t st v}
+        : type.and_for_each_lhs_of_arrow (t:=t) (@abstraction_relation) st v -> type.and_for_each_lhs_of_arrow (t:=t) (@type.eqv) v v.
+      Proof using Type.
+        apply type.and_for_each_lhs_of_arrow_Proper_impl_hetero2, @eqv_refl_of_abstraction_relation.
+      Qed.
+      Local Hint Immediate eqv_refl_of_abstraction_relation_for_each_lhs_of_arrow : core typeclass_instances.
 
-      Lemma bottom_for_each_lhs_of_arrow_related t v : type.and_for_each_lhs_of_arrow (@abstraction_relation) (@bottom_for_each_lhs_of_arrow t) v.
-      Proof using bottom'_related. induction t; cbn; eauto using bottom_related. Qed.
+      Lemma abstract_domain_R_refl_of_abstraction_relation_for_each_lhs_of_arrow {t st v}
+        : type.and_for_each_lhs_of_arrow (t:=t) (@abstraction_relation) st v -> type.and_for_each_lhs_of_arrow (t:=t) (@abstract_domain_R) st st.
+      Proof using abstract_domain'_R_of_related.
+        apply type.and_for_each_lhs_of_arrow_Proper_impl_hetero1, @abstract_domain_R_refl_of_abstraction_relation.
+      Qed.
+      Local Hint Immediate abstract_domain_R_refl_of_abstraction_relation_for_each_lhs_of_arrow : core typeclass_instances.
+
+      Lemma abstraction_relation_iff_app_curried {t st v}
+        : @abstraction_relation t st v
+          <-> (Proper (@abstract_domain_R t) st
+               /\ v == v
+               /\ forall x y,
+                  type.and_for_each_lhs_of_arrow (@abstraction_relation) x y
+                  -> abstraction_relation' _ (type.app_curried st x) (type.app_curried v y)).
+      Proof using abstract_domain'_R_of_related.
+        apply type.related_hetero_and_Proper_iff_app_curried; eauto; repeat intro; hnf; eauto.
+      Qed.
 
       Local Notation bottom_Proper := (@bottom_Proper base_type abstract_domain' bottom' abstract_domain'_R bottom'_Proper).
       Local Notation bottom_for_each_lhs_of_arrow_Proper := (@bottom_for_each_lhs_of_arrow_Proper base_type abstract_domain' bottom' abstract_domain'_R bottom'_Proper).
 
       Local Hint Resolve (@bottom_Proper) (@bottom_for_each_lhs_of_arrow_Proper) : core typeclass_instances.
 
-      Fixpoint related_bounded_value {t} : abstract_domain t -> value t -> type.interp base_interp t -> Prop
-        := match t return abstract_domain t -> value t -> type.interp base_interp t -> Prop with
+      Lemma bottom_related t v : v == v -> @abstraction_relation t bottom v.
+      Proof using bottom'_Proper bottom'_related.
+        induction t; cbv [abstraction_relation]; cbn [type.related_hetero_and_Proper]; cbv [respectful_hetero]; repeat split; eauto.
+        repeat intro; cbn.
+        repeat first [ do_with_exactly_one_hyp ltac:(fun H => apply H)
+                     | eassumption
+                     | eapply eqv_refl_of_abstraction_relation ].
+      Qed.
+
+      Local Hint Immediate bottom_related : core typeclass_instances.
+
+      Lemma related_bottom_for_each_lhs_of_arrow t v : type.and_for_each_lhs_of_arrow (@type.eqv) v v -> type.and_for_each_lhs_of_arrow (@abstraction_relation) (@bottom_for_each_lhs_of_arrow t) v.
+      Proof using bottom'_Proper bottom'_related. induction t; cbn; split; split_and; eauto using bottom_related. Qed.
+      Local Hint Immediate related_bottom_for_each_lhs_of_arrow : core.
+
+      Lemma related_bottom_for_each_lhs_of_arrow_hetero_eqv_l t v v' : type.and_for_each_lhs_of_arrow (@type.eqv) v v' -> type.and_for_each_lhs_of_arrow (@abstraction_relation) (@bottom_for_each_lhs_of_arrow t) v.
+      Proof using bottom'_Proper bottom'_related. intro; apply related_bottom_for_each_lhs_of_arrow; etransitivity; (idtac + symmetry); eassumption. Qed.
+      Lemma related_bottom_for_each_lhs_of_arrow_hetero_eqv_r t v v' : type.and_for_each_lhs_of_arrow (@type.eqv) v' v -> type.and_for_each_lhs_of_arrow (@abstraction_relation) (@bottom_for_each_lhs_of_arrow t) v.
+      Proof using bottom'_Proper bottom'_related. intro; apply related_bottom_for_each_lhs_of_arrow; etransitivity; (idtac + symmetry); eassumption. Qed.
+      Local Hint Immediate related_bottom_for_each_lhs_of_arrow_hetero_eqv_l related_bottom_for_each_lhs_of_arrow_hetero_eqv_r : core.
+
+      Fixpoint related_bounded_value' {t} : abstract_domain t -> value' t -> type.interp base_interp t -> Prop
+        := match t return abstract_domain t -> value' t -> type.interp base_interp t -> Prop with
            | type.base t
-             => fun st '(e_st, e) v
-                => abstract_domain'_R t st e_st
-                   /\ expr.interp ident_interp e = v
+             => fun st e v
+                => expr.interp ident_interp e = v
                    /\ abstraction_relation' t st v
            | type.arrow s d
              => fun st e v
                => Proper type.eqv v
-                 /\ forall st_s e_s v_s,
-                   let st_s := match s with
-                               | type.base _ => st_s
-                               | type.arrow _ _ => bottom
-                               end in
-                   @related_bounded_value s st_s e_s v_s
-                   -> @related_bounded_value d (st st_s) (UnderLets.interp ident_interp (e e_s)) (v v_s)
+                  /\ Proper abstract_domain_R st
+                  /\ forall st_s e_s v_s,
+                   @related_bounded_value' s st_s e_s v_s
+                   -> @related_bounded_value' d (st st_s) (UnderLets.interp ident_interp (e (st_s, e_s))) (v v_s)
            end.
-      Definition related_bounded_value_with_lets {t} : abstract_domain t -> value_with_lets t -> type.interp base_interp t -> Prop
-        := fun st e v => related_bounded_value st (UnderLets.interp ident_interp e) v.
+      Definition related_bounded_value {t} : value t -> type.interp base_interp t -> Prop
+        := fun st_e v => related_bounded_value' (state_of_value st_e) (UnderLets.interp ident_interp (project_value' st_e)) v.
 
-      Definition related_of_related_bounded_value {t} st e v
-        : @related_bounded_value t st e v -> v == v.
+      Definition related_of_related_bounded_value' {t} st e v
+        : @related_bounded_value' t st e v -> v == v.
       Proof using Type. destruct t; [ reflexivity | intros [? ?]; assumption ]. Qed.
 
       Lemma abstract_domain'_R_refl_of_rel_l t x y (H : @abstract_domain'_R t x y)
@@ -199,43 +253,35 @@ Module Compilers.
 
       Local Hint Immediate abstract_domain_R_refl_of_rel_l abstract_domain_R_refl_of_rel_r : core.
 
-      Lemma related_bottom_for_each_lhs_of_arrow {t} v
-        : type.and_for_each_lhs_of_arrow (@abstraction_relation) (@bottom_for_each_lhs_of_arrow t) v.
-      Proof using bottom'_related. induction t; cbn; eauto. Qed.
-
-      Local Hint Immediate related_bottom_for_each_lhs_of_arrow : core.
-
-      Fixpoint fill_in_bottom_for_arrows {t} : abstract_domain t -> abstract_domain t
-        := match t with
-           | type.base t => fun x => x
-           | type.arrow s d
-             => fun f x => let x := match s with
-                                | type.base _ => x
-                                | type.arrow _ _ => bottom
-                                end in
-                       @fill_in_bottom_for_arrows d (f x)
-           end.
-
-      Lemma abstract_domain_R_bottom_fill_arrows {t}
-        : abstract_domain_R (@bottom t) (fill_in_bottom_for_arrows (@bottom t)).
-      Proof using bottom'_Proper.
-        cbv [abstract_domain_R]; induction t as [t|s IHs d IHd]; cbn [fill_in_bottom_for_arrows bottom type.related];
-          cbv [respectful Proper] in *; auto.
+      Definition abstract_domain_R_of_related_bounded_value' {t} st e v
+        : @related_bounded_value' t st e v -> abstract_domain_R st st.
+      Proof using abstract_domain'_R_of_related.
+        destruct t; [ cbn; intros [? ?]; subst; eapply abstract_domain'_R_of_related; eassumption | intros [? ?]; destruct_head'_and; assumption ].
       Qed.
 
-      Lemma fill_in_bottom_for_arrows_bottom_related {t} v
-        : abstraction_relation (fill_in_bottom_for_arrows (@bottom t)) v.
-      Proof using bottom'_related.
-        cbv [abstraction_relation]; induction t; cbn; cbv [respectful_hetero]; eauto.
+      Lemma abstraction_relation_Proper_iff {t} : Proper (abstract_domain_R ==> type.eqv ==> iff) (@abstraction_relation t).
+      Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper.
+        apply @type.related_hetero_and_Proper_Proper_iff; try exact _.
+        all: try now repeat intro; split; subst; eapply abstraction_relation'_Proper; (idtac + symmetry); auto; eassumption.
+        all: try now apply abstract_domain'_R_of_related.
       Qed.
 
-      Hint Resolve fill_in_bottom_for_arrows_bottom_related : core.
+      Lemma abstraction_relation_Proper_iff_abstract_domain_R {t} : Proper (abstract_domain_R ==> eq ==> iff) (@abstraction_relation t).
+      Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper.
+        repeat intro; subst.
+        match goal with |- ?A <-> ?B => cut (A \/ B -> (A <-> B)); [ tauto | ] end.
+        intro H'.
+        apply abstraction_relation_Proper_iff; try assumption.
+        destruct_head'_or; eapply eqv_refl_of_abstraction_relation; eassumption.
+      Qed.
 
-      Local Instance fill_in_bottom_for_arrows_Proper {t} : Proper (abstract_domain_R ==> abstract_domain_R) (@fill_in_bottom_for_arrows t).
-      Proof using bottom'_Proper.
-        pose proof (@bottom_Proper).
-        cbv [Proper respectful abstract_domain_R] in *; induction t; cbn in *; cbv [respectful] in *;
-          intros; break_innermost_match; eauto.
+      Lemma abstraction_relation_Proper_iff_eqv {t} : Proper (eq ==> type.eqv ==> iff) (@abstraction_relation t).
+      Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper.
+        repeat intro; subst.
+        match goal with |- ?A <-> ?B => cut (A \/ B -> (A <-> B)); [ tauto | ] end.
+        intro H'.
+        apply abstraction_relation_Proper_iff; try assumption.
+        destruct_head'_or; eapply abstract_domain_R_refl_of_abstraction_relation; eassumption.
       Qed.
 
       Local Instance bottom_eqv_Proper_refl {t} : Proper type.eqv (@bottom t).
@@ -245,179 +291,133 @@ Module Compilers.
       Proof using Type. apply bottom_eqv_Proper_refl. Qed.
       Local Hint Resolve bottom_eqv_refl : core.
 
-      Local Instance fill_in_bottom_for_arrows_Proper_eqv {t} : Proper (type.eqv ==> type.eqv) (@fill_in_bottom_for_arrows t).
-      Proof using Type.
-        cbv [Proper respectful] in *; induction t; cbn in *; cbv [respectful] in *;
-          intros; break_innermost_match; cbn in *; cbv [respectful] in *; eauto.
-      Qed.
-
-      Lemma state_of_value_related_fill {t} v (HP : Proper abstract_domain_R (@state_of_value t v))
-        : abstract_domain_R (@state_of_value t v) (fill_in_bottom_for_arrows (@state_of_value t v)).
-      Proof using bottom'_Proper. destruct t; [ assumption | apply abstract_domain_R_bottom_fill_arrows ]. Qed.
-
-      Lemma eqv_bottom_fill_bottom {t}
-        : @bottom t == fill_in_bottom_for_arrows bottom.
-      Proof using Type. induction t; cbn; [ reflexivity | ]; cbv [respectful]; auto. Qed.
-
-      Lemma eqv_fill_bottom_idempotent {t} v1 v2
-        : v1 == v2 -> fill_in_bottom_for_arrows (fill_in_bottom_for_arrows v1) == @fill_in_bottom_for_arrows t v2.
-      Proof using Type. induction t; cbn; cbv [respectful]; break_innermost_match; auto. Qed.
-
-      Lemma abstract_domain_R_fill_bottom_idempotent {t} v1 v2
-        : abstract_domain_R v1 v2
-          -> abstract_domain_R (fill_in_bottom_for_arrows (fill_in_bottom_for_arrows v1))
-                               (@fill_in_bottom_for_arrows t v2).
-      Proof using bottom'_Proper.
-        pose proof (@bottom_Proper) as Hb.
-        induction t as [|s IHs d IHd]; cbn; cbv [respectful Proper abstract_domain_R] in *; break_innermost_match; auto.
+      Lemma related_refl_of_related_bounded_value' {t} st e v
+        : @related_bounded_value' t st e v -> abstract_domain_R st st.
+      Proof using abstract_domain'_R_of_related.
+        destruct t; cbn; break_innermost_match; intros; destruct_head'_and; try assumption.
+        eapply abstract_domain'_R_of_related; eassumption.
       Qed.
 
-      Lemma app_curried_state_of_value_fill {t} v x y
-            (H : type.and_for_each_lhs_of_arrow (@type.eqv) x y)
-        : type.app_curried (@state_of_value t v) x = type.app_curried (fill_in_bottom_for_arrows (@state_of_value t v)) y.
-      Proof using Type.
-        destruct t; [ reflexivity | cbv [state_of_value] ].
-        apply type.app_curried_Proper; [ apply eqv_bottom_fill_bottom | assumption ].
-      Qed.
-
-      Lemma first_order_app_curried_fill_in_bottom_for_arrows_eq {t} f xs
-            (Ht : type.is_not_higher_order t = true)
-        : type.app_curried (t:=t) f xs = type.app_curried (fill_in_bottom_for_arrows f) xs.
-      Proof using Type.
-        clear -Ht.
-        induction t as [| [|s' d'] IHs d IHd]; cbn in *; try discriminate; auto.
-      Qed.
-
-      Lemma first_order_abstraction_relation_fill_in_bottom_for_arrows_iff
-            {t} f v
-            (Ht : type.is_not_higher_order t = true)
-        : @abstraction_relation t f v
-          <-> @abstraction_relation t (fill_in_bottom_for_arrows f) v.
-      Proof using Type.
-        clear -Ht; cbv [abstraction_relation].
-        split; induction t as [| [|s' d'] IHs d IHd];
-          cbn in *; cbv [respectful_hetero]; try discriminate; auto.
-      Qed.
-
-      Lemma related_state_of_value_of_related_bounded_value {t} st e v
-        : @related_bounded_value t st e v -> abstract_domain_R match t with
-                                                              | type.base _ => st
-                                                              | type.arrow _ _ => bottom
-                                                              end (state_of_value e).
-      Proof using bottom'_Proper. intro H; destruct t; cbn in *; [ destruct e; apply H | repeat intro; refine bottom_Proper ]. Qed.
-
-      Lemma related_state_of_value_of_related_bounded_value2 {t} st e v (st' := match t with
-                                                                                | type.base _ => st
-                                                                                | type.arrow _ _ => bottom
-                                                                                end)
-        : @related_bounded_value t st' e v -> abstract_domain_R st' (state_of_value e).
-      Proof using bottom'_Proper. intro H; destruct t; cbn in *; [ destruct e; apply H | repeat intro; refine bottom_Proper ]. Qed.
-
-      Lemma related_bounded_value_Proper {t} st1 st2 (Hst : abstract_domain_R (fill_in_bottom_for_arrows st1) (fill_in_bottom_for_arrows st2))
+      Lemma related_bounded_value'_Proper {t} st1 st2 (Hst : abstract_domain_R st1 st2)
             a a1 a2
             (Ha' : type.eqv a1 a2)
-        : @related_bounded_value t st1 a a1 -> @related_bounded_value t st2 a a2.
-      Proof using abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_Proper.
-        induction t as [t|s IHs d IHd]; cbn [related_bounded_value type.related] in *; cbv [respectful abstract_domain_R] in *.
-        all: cbn [type.andb_each_lhs_of_arrow] in *.
-        all: rewrite ?Bool.andb_true_iff in *.
-        all: destruct_head'_and.
-        { intros; break_innermost_match; subst;
-            destruct_head'_and; repeat apply conj; auto.
-          { etransitivity; (idtac + symmetry); eassumption. }
-          { eapply abstraction_relation'_Proper; (eassumption + reflexivity). } }
+        : @related_bounded_value' t st1 a a1 -> @related_bounded_value' t st2 a a2.
+      Proof using abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric abstract_domain'_R_of_related.
+        induction t as [t|s IHs d IHd]; cbn [related_bounded_value' type.related] in *; cbv [respectful abstract_domain_R] in *.
+        all: subst.
+        { intros; destruct_head'_and; subst; repeat apply conj; try reflexivity.
+          eapply abstraction_relation'_Proper; (eassumption + reflexivity). }
         { intros [? Hrel].
-          split; [ repeat intro; etransitivity; (idtac + symmetry); eapply Ha'; (eassumption + (etransitivity; (idtac + symmetry); eassumption)) | ].
-          pose proof (@bottom_Proper s) as Hsbot.
-          intros ?? v_s; destruct s; intros Hx; cbn [type.related] in *;
-            cbn [fill_in_bottom_for_arrows] in *; cbv [respectful] in *.
-          { specialize_by_assumption; cbn in *.
-            eapply IHd; [ cbn in Hst |- *; eapply Hst | apply Ha'; reflexivity | eapply Hrel, Hx ]; cbv [respectful].
-            cbn [related_bounded_value] in *.
-            break_innermost_match_hyps; destruct_head'_and.
-            eauto. }
-          { eapply IHd; [ eapply Hst | apply Ha' | eapply Hrel, Hx ];
-              [ eexact Hsbot | refine (@related_of_related_bounded_value _ _ _ v_s _); eassumption | refine bottom ]. } }
+          split; [ | split ];
+            [ repeat intro; etransitivity; (idtac + symmetry); (eapply Ha' + eapply Hst); (eassumption + (etransitivity; (idtac + symmetry); eassumption)) ..
+            | ].
+          { intros ?? v_s Hx; cbn [type.related] in *; cbv [respectful] in *.
+            eapply IHd; [ cbn in Hst |- *; eapply Hst | apply Ha' | eapply Hrel, Hx ].
+            all: try now eapply related_refl_of_related_bounded_value'; eassumption.
+            all: try now eapply related_of_related_bounded_value'; eassumption. } }
       Qed.
 
-      Lemma related_bounded_value_fill_bottom_iff {t} st1 st2 (Hst : abstract_domain_R st1 st2)
-            a a1 a2
-            (Ha' : type.eqv a1 a2)
-        : @related_bounded_value t st1 a a1 <-> @related_bounded_value t (fill_in_bottom_for_arrows st2) a a2.
-      Proof using abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_Proper.
-        split; eapply related_bounded_value_Proper; try solve [ (idtac + symmetry); assumption ].
-        all: (idtac + symmetry); apply abstract_domain_R_fill_bottom_idempotent.
-        all: (idtac + symmetry); assumption.
+      Lemma related_bounded_value'_Proper1 {t}
+        : Proper (abstract_domain_R ==> eq ==> eq ==> Basics.impl) (@related_bounded_value' t).
+      Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper.
+        repeat intro; subst; eapply related_bounded_value'_Proper; try eassumption.
+        eapply related_of_related_bounded_value'; eassumption.
       Qed.
 
-      Lemma related_bounded_value_Proper1 {t}
-        : Proper (abstract_domain_R ==> eq ==> eq ==> Basics.impl) (@related_bounded_value t).
-      Proof using abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_Proper.
-        repeat intro; subst; eapply related_bounded_value_Proper.
-        { eapply fill_in_bottom_for_arrows_Proper; eassumption. }
-        { eapply related_of_related_bounded_value; eassumption. }
-        { assumption. }
+      Lemma related_bounded_value'_Proper3 {t}
+        : Proper (eq ==> eq ==> type.eqv ==> Basics.impl) (@related_bounded_value' t).
+      Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper.
+        repeat intro; subst; eapply related_bounded_value'_Proper; try eassumption.
+        eapply abstract_domain_R_of_related_bounded_value'; eassumption.
       Qed.
 
-      Lemma related_bounded_value_Proper_eq {t}
-        : Proper (eq ==> eq ==> eq ==> Basics.impl) (@related_bounded_value t).
+      Lemma related_bounded_value'_Proper_eq {t}
+        : Proper (eq ==> eq ==> eq ==> Basics.impl) (@related_bounded_value' t).
       Proof using Type.
         repeat intro; subst; assumption.
       Qed.
 
-      Lemma related_bounded_value_Proper_interp_eq_base {t}
-        : Proper (eq ==> RelProd eq (fun x y => expr.interp ident_interp x = expr.interp ident_interp y) ==> eq ==> Basics.impl) (@related_bounded_value (type.base t)).
+      Lemma related_bounded_value'_Proper_interp_eq_base {t}
+        : Proper (eq ==> (fun x y => expr.interp ident_interp x = expr.interp ident_interp y) ==> eq ==> Basics.impl) (@related_bounded_value' (type.base t)).
       Proof using Type.
         repeat intro; subst.
-        cbv [value RelProd relation_conjunction predicate_intersection pointwise_extension RelCompFun] in *.
-        destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *; subst.
-        cbv [related_bounded_value] in *; destruct_head'_and; repeat apply conj; subst; (idtac + symmetry); assumption.
+        cbv [related_bounded_value'] in *; destruct_head'_and; repeat apply conj; subst; (idtac + symmetry); assumption.
+      Qed.
+
+      Lemma state_of_value_reflect is_let_bound {t} e st
+        : state_of_value (@reflect is_let_bound t e st) = st.
+      Proof using Type. destruct t; reflexivity. Qed.
+
+      Lemma related_bounded_value'_of_abstraction_relation_of_reflect
+        {t} {annotate_with_state}
+        (interp_reflect
+           : forall st e v
+                    (H_val : expr.interp ident_interp e == v)
+                    (Hst1 : abstraction_relation st (expr.interp ident_interp e)),
+            related_bounded_value
+              (@reflect annotate_with_state t e st)
+              v)
+        st v
+        (H : abstraction_relation st v)
+        : @related_bounded_value' t st (UnderLets.interp ident_interp (project_value' (@reflect annotate_with_state t (expr.Var v) st))) v.
+      Proof using Type.
+        specialize (interp_reflect st (expr.Var v) v).
+        cbv [related_bounded_value] in interp_reflect.
+        rewrite state_of_value_reflect in interp_reflect.
+        apply interp_reflect; try assumption.
+        eapply eqv_refl_of_abstraction_relation; eassumption.
       Qed.
 
       Fixpoint interp_reify
-               annotate_with_state is_let_bound {t} st e v b_in
-               (Hb : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) b_in)
-               (H : related_bounded_value st e v) {struct t}
-        : (forall arg1 arg2
-                  (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
-                  (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1),
-              type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1
-              = type.app_curried v arg2)
-          /\ (forall arg1
-                     (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1)
-                     (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1),
-                 abstraction_relation'
-                   _
-                   (type.app_curried (fill_in_bottom_for_arrows st) b_in)
-                   (type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1))
+        annotate_with_state is_let_bound {t} e v b_in
+        (H : related_bounded_value e v)
+        {struct t}
+        : forall arg1 arg2
+                 (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
+                 (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1),
+          type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1
+          = type.app_curried v arg2
       with interp_reflect
              annotate_with_state {t} st e v
-             (Hst_Proper : Proper abstract_domain_R st)
+             (*(Hst_Proper : Proper abstract_domain_R st)*) (* follows from abstraction relation *)
              (H_val : expr.interp ident_interp e == v)
-             (Hst1 : abstraction_relation (fill_in_bottom_for_arrows st) (expr.interp ident_interp e))
+             (Hst1 : abstraction_relation st (expr.interp ident_interp e))
              {struct t}
            : related_bounded_value
-               st
                (@reflect annotate_with_state t e st)
-               v.
-      Proof using interp_annotate abstraction_relation'_Proper bottom'_related bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric.
+               v
+      with abstraction_relation_of_related_bounded_value'
+             {t} st e v
+             {struct t}
+        : @related_bounded_value' t st e v
+          -> abstraction_relation st v.
+      Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper bottom'_Proper bottom'_related interp_annotate.
         all: destruct t as [t|s d];
-          [ clear interp_reify interp_reflect
-          | pose proof (fun is_let_bound => interp_reify annotate_with_state is_let_bound s) as interp_reify_s;
-            pose proof (fun is_let_bound => interp_reify annotate_with_state is_let_bound d) as interp_reify_d;
-            pose proof (interp_reflect annotate_with_state s) as interp_reflect_s;
-            pose proof (interp_reflect annotate_with_state d) as interp_reflect_d;
-            clear interp_reify interp_reflect;
-            pose proof (@abstract_domain_R_bottom_fill_arrows s);
-            pose proof (@abstract_domain_R_bottom_fill_arrows d) ].
+          [ clear interp_reify interp_reflect abstraction_relation_of_related_bounded_value'
+          | pose proof (fun annotate_with_state is_let_bound => interp_reify annotate_with_state is_let_bound s) as interp_reify_s;
+            pose proof (fun annotate_with_state is_let_bound => interp_reify annotate_with_state is_let_bound d) as interp_reify_d;
+            pose proof (fun annotate_with_state => interp_reflect annotate_with_state s) as interp_reflect_s;
+            pose proof (fun annotate_with_state => interp_reflect annotate_with_state d) as interp_reflect_d;
+            pose proof (abstraction_relation_of_related_bounded_value' s) as abstraction_relation_of_related_bounded_value'_s;
+            pose proof (abstraction_relation_of_related_bounded_value' d) as abstraction_relation_of_related_bounded_value'_d;
+            pose proof (@related_bounded_value'_of_abstraction_relation_of_reflect s false (interp_reflect_s false)) as related_bounded_value'_of_abstraction_relation_s;
+            pose proof (@related_bounded_value'_of_abstraction_relation_of_reflect d false (interp_reflect_d false)) as related_bounded_value'_of_abstraction_relation_d;
+            try specialize (interp_reify_s annotate_with_state);
+            try specialize (interp_reify_d annotate_with_state);
+            try specialize (interp_reflect_s annotate_with_state);
+            try specialize (interp_reflect_d annotate_with_state);
+            clear interp_reify interp_reflect abstraction_relation_of_related_bounded_value' ].
+        all: cbv [abstraction_relation] in *; cbn [type.related_hetero_and_Proper] in *; cbv [respectful_hetero] in *.
         all: cbn [reify reflect] in *; fold (@reify) (@reflect) in *.
-        all: cbn [related_bounded_value type.related type.app_curried] in *.
-        all: cbn [UnderLets.interp expr.interp type.final_codomain type.andb_each_lhs_of_arrow type.is_base fst snd fill_in_bottom_for_arrows type.map_for_each_lhs_of_arrow type.for_each_lhs_of_arrow type.and_for_each_lhs_of_arrow partial.bottom_for_each_lhs_of_arrow partial.bottom] in *.
-        all: destruct annotate_with_state; try destruct is_let_bound.
+        all: cbn [related_bounded_value' type.related type.app_curried] in *.
+        all: cbn [UnderLets.interp expr.interp type.final_codomain type.andb_each_lhs_of_arrow type.is_base fst snd type.map_for_each_lhs_of_arrow type.for_each_lhs_of_arrow type.and_for_each_lhs_of_arrow partial.bottom_for_each_lhs_of_arrow partial.bottom] in *.
+        all: try destruct annotate_with_state; try destruct is_let_bound.
+        all: change (type.related_hetero_and_Proper abstract_domain'_R (fun t : base_type => eq) abstraction_relation' (t:=?t)) with (@abstraction_relation t) in *.
         all: repeat first [ reflexivity
+                          | assumption
                           | progress eta_expand
-                          | progress cbv [type.is_not_higher_order] in *
                           | progress cbn [UnderLets.interp expr.interp type.final_codomain fst snd] in *
+                          | progress cbn [state_of_value project_value' fst snd Base_value' UnderLets.interp] in *
                           | progress subst
                           | progress destruct_head'_and
                           | progress destruct_head'_prod
@@ -437,84 +437,102 @@ Module Compilers.
                           | match goal with
                             | [ H : fst ?x = _ |- _ ] => is_var x; destruct x
                             | [ H : Proper _ ?st |- ?R (?st _) (?st _) ] => apply H
-                            | [ |- ?R (state_of_value _) (state_of_value _) ] => cbv [state_of_value] in *
+                            | [ |- type.related _ ?x ?x ]
+                              => eapply related_refl_of_related_bounded_value'; eassumption
+                            end
+                          | match goal with
+                            | [ H' : ?R ?i, H : forall a b, ?R a /\ @?A b -> @?B b |- _ ]
+                              => specialize (fun b H'' => H i b (conj H' H''))
+                            | [ H' : ?R ?i, H : forall a b, @?A a /\ ?R b -> @?B a |- _ ]
+                              => specialize (fun a H'' => H a i (conj H'' H'))
                             end
                           | solve [ repeat intro; apply bottom_Proper
-                                  | auto; cbv [Proper respectful Basics.impl] in *; eauto ]
+                                  | auto; cbv [Proper respectful Basics.impl] in *; eauto
+                                  | eapply related_refl_of_related_bounded_value'; eassumption
+                                  | eapply related_bottom_for_each_lhs_of_arrow, eqv_refl_of_abstraction_relation_for_each_lhs_of_arrow; eassumption
+                                  | eapply abstract_domain_R_refl_of_abstraction_relation; eassumption ]
                           | progress (repeat apply conj; intros * )
                           | progress intros
                           | progress destruct_head'_or
-                          | do_with_exactly_one_hyp ltac:(fun H => eapply H; clear H);
-                            try assumption; auto; []
                           | match goal with
                             | [ |- Proper ?R _ ] => (eapply PER_valid_l + eapply PER_valid_r); eassumption
-                            | [ |- @related_bounded_value ?t ?st1 (reflect _ _ ?st2) _ ]
-                              => (tryif first [ constr_eq st1 st2 | has_evar st1 | has_evar st2 ]
-                                  then fail
-                                  else (eapply (@related_bounded_value_Proper1 t st2 st1);
-                                        try reflexivity))
                             | [ H : ?R ?x ?y |- ?R ?y ?x ] => symmetry; assumption
                             end
-                          | break_innermost_match_step
-                          | do_with_exactly_one_hyp ltac:(fun H => eapply H; clear H);
-                            try assumption; auto
                           | match goal with
-                            | [ |- abstraction_relation (fill_in_bottom_for_arrows (?f (state_of_value ?e))) _ ]
-                              => replace (state_of_value e) with (match s with
-                                                                 | type.base _ => state_of_value e
-                                                                 | type.arrow _ _ => bottom
-                                                                 end) by (destruct s; reflexivity)
+                            | [ H : related_bounded_value' ?st ?e ?v |- related_bounded_value' ?st ?e' ?v' ]
+                              => is_evar e'; unify e e';
+                                 eapply related_bounded_value'_Proper3; [ reflexivity .. | symmetry | exact H ]
+                            | [ H' : abstraction_relation ?stv ?vv, H : forall annotate_with_state st e v, _ == v -> abstraction_relation st (expr.interp _ e) -> related_bounded_value (reflect annotate_with_state e st) v |- related_bounded_value' ?stv ?ee ?vv ]
+                              => is_evar ee;
+                                 specialize (H false stv (expr.Var vv) vv);
+                                 cbv [related_bounded_value] in H;
+                                 rewrite state_of_value_reflect in H; eapply H; clear H
                             end
-                          | progress fold (@reify) (@reflect) (@type.interp) (@type.related) (@type.related_hetero) in *
+                          | break_innermost_match_step
+                          | progress fold (@reify) (@reflect) (@type.interp) (@type.related) (@type.related_hetero) (@related_bounded_value') (@abstraction_relation) in *
                           | match goal with
+                            | [ H : forall a b c d e (f : bool), _ |- _ ]
+                              => unique pose proof (fun a b c d e => H a b c d e true);
+                                 unique pose proof (fun a b c d e => H a b c d e false);
+                                 clear H
                             | [ |- type.related _ (expr.interp _ (UnderLets.interp _ (reify _ _ _ _))) _ ]
                               => rewrite type.related_iff_app_curried
-                            | [ |- type.related_hetero _ (@state_of_value ?t _) _ ]
-                              => is_var t; destruct t; cbv [state_of_value]; [ cbn | apply bottom_related ]
-                            end ].
+                            | [ interp_reflect_d : context[_ -> related_bounded_value (reflect _ _ _) _] |- related_bounded_value' ?st (UnderLets.interp _ (project_value' (reflect _ ?e ?st))) ?v ]
+                              => specialize (interp_reflect_d st e v);
+                                 cbv [related_bounded_value] in interp_reflect_d;
+                                 rewrite state_of_value_reflect in interp_reflect_d
+                            | [ H : context[_ -> type.app_curried (expr.interp _ (UnderLets.interp _ (reify ?b _ _ _))) _ = _] |- type.app_curried (expr.interp _ (UnderLets.interp _ (reify ?b ?is_let_bound ?e ?b_in))) ?arg = _ ]
+                              => apply H; clear H
+                            | [ H : context[_ -> abstraction_relation' _ (type.app_curried _ _) (type.app_curried (expr.interp _ (UnderLets.interp _ (reify ?b _ _ _))) _)]
+                                |- abstraction_relation' _ (type.app_curried _ ?x) (type.app_curried (expr.interp _ (UnderLets.interp _ (reify ?b ?is_let_bound ?e ?b_in))) ?arg) ]
+                              => specialize (H is_let_bound e); cbn [state_of_value Base_value' fst] in H;
+                                 eapply H; clear H
+                            | [ |- related_bounded_value (_, Base _) _ ] => hnf; cbn [state_of_value project_value' Base_value' UnderLets.interp fst snd]
+                            | [ H : forall st e v, _ -> related_bounded_value' _ (UnderLets.interp _ (?u _)) _ |- related_bounded_value' _ (UnderLets.interp _ (?u _)) _ ]
+                              => apply H; clear H
+                            | [ H : context[_ -> related_bounded_value' _ _ _ -> abstraction_relation _ _] |- abstraction_relation _ _ ]
+                              => eapply H; clear H
+                            end
+                          | match goal with
+                            | [ H : forall x : _ * _, _ |- _ ] => specialize (fun a b => H (a, b))
+                            end
+                          | rewrite state_of_value_reflect
+                          | rewrite type.related_hetero_iff_app_curried
+                          | do_with_exactly_one_hyp ltac:(fun H => apply H; clear H) ].
       Qed.
 
-      Lemma interp_reify_first_order
-               annotate_with_state is_let_bound {t} st e v b_in
-               (Ht : type.is_not_higher_order t = true)
-               (Hb : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) b_in)
-               (H : related_bounded_value st e v)
-        : (forall arg1 arg2
-                  (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
-                  (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1),
-              type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1
-              = type.app_curried v arg2)
-          /\ (forall arg1
-                     (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1)
-                     (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1),
-                 abstraction_relation'
-                   _
-                   (type.app_curried st b_in)
-                   (type.app_curried (expr.interp ident_interp (UnderLets.interp ident_interp (@reify annotate_with_state is_let_bound t e b_in))) arg1)).
-      Proof using interp_annotate abstraction_relation'_Proper bottom'_related bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric.
-        rewrite first_order_app_curried_fill_in_bottom_for_arrows_eq by assumption.
-        apply interp_reify; assumption.
+      Lemma related_bounded_value'_of_abstraction_relation_annotate_with_state
+        {t} {annotate_with_state} st v
+        (H : abstraction_relation st v)
+        : @related_bounded_value' t st (UnderLets.interp ident_interp (project_value' (@reflect annotate_with_state t (expr.Var v) st))) v.
+      Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper bottom'_Proper bottom'_related interp_annotate.
+        apply related_bounded_value'_of_abstraction_relation_of_reflect; try assumption.
+        apply @interp_reflect.
       Qed.
 
-      Lemma interp_reflect_first_order
-             annotate_with_state {t} st e v
-             (Ht : type.is_not_higher_order t = true)
-             (Hst_Proper : Proper abstract_domain_R st)
-             (H_val : expr.interp ident_interp e == v)
-             (Hst : abstraction_relation st (expr.interp ident_interp e))
-        : related_bounded_value
-            st
-            (@reflect annotate_with_state t e st)
-            v.
-      Proof using interp_annotate abstraction_relation'_Proper bottom'_related bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric.
-        rewrite first_order_abstraction_relation_fill_in_bottom_for_arrows_iff in Hst by assumption.
-        apply interp_reflect; assumption.
+      Lemma related_bounded_value'_of_abstraction_relation
+        {t} st v
+        (H : abstraction_relation st v)
+        : @related_bounded_value' t st (UnderLets.interp ident_interp (project_value' (@reflect false t (expr.Var v) st))) v.
+      Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper bottom'_Proper bottom'_related interp_annotate.
+        apply related_bounded_value'_of_abstraction_relation_annotate_with_state; assumption.
+      Qed.
+
+      Lemma abstraction_relation_of_related_bounded_value'_app_curried
+        {t} st e v b_in arg
+        (H : @related_bounded_value' t st e v)
+        (Harg : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg)
+        : abstraction_relation' _ (type.app_curried st b_in) (type.app_curried v arg).
+      Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper bottom'_Proper bottom'_related interp_annotate.
+        pose proof (@abstraction_relation_of_related_bounded_value' t st e v H) as H'.
+        rewrite abstraction_relation_iff_app_curried in H'.
+        apply H'; assumption.
       Qed.
 
       Lemma related_bounded_value_annotate_base {t}
             v_st st v
-        : @related_bounded_value (type.base t) v_st st v
-          -> @related_bounded_value (type.base t) v_st (fst st, UnderLets.interp ident_interp (annotate true t (fst st) (snd st))) v.
+        : @related_bounded_value' (type.base t) v_st st v
+          -> @related_bounded_value' (type.base t) v_st (UnderLets.interp ident_interp (annotate true t v_st st)) v.
       Proof using interp_annotate abstraction_relation'_Proper.
         clear -interp_annotate abstraction_relation'_Proper.
         cbv [Proper respectful Basics.impl] in *.
@@ -523,136 +541,157 @@ Module Compilers.
         rewrite interp_annotate by eauto; reflexivity.
       Qed.
 
-      Lemma related_bounded_value_bottomify {t} v_st st v
-        : @related_bounded_value t v_st st v
-          -> @related_bounded_value t bottom (UnderLets.interp ident_interp (bottomify st)) v.
-      Proof using bottom'_Proper bottom'_related.
-        induction t; cbn in *;
-          repeat first [ progress subst
-                       | progress cbv [respectful] in *
-                       | progress cbn [UnderLets.interp] in *
-                       | progress destruct_head'_and
-                       | break_innermost_match_step
-                       | progress intros
-                       | apply conj
-                       | reflexivity
-                       | apply bottom'_Proper
-                       | apply bottom'_related
-                       | solve [ eauto ]
-                       | rewrite UnderLets.interp_splice ].
+      Lemma interp_extract_gen_from_wf_gen G
+        (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> abstract_domain_R v1 v2)
+        {t} (e1 e2 : expr t) b_in1 b_in2
+        (Hwf : expr.wf G e1 e2)
+        (Hb_in : type.and_for_each_lhs_of_arrow (@abstract_domain_R) b_in1 b_in2)
+        : abstract_domain'_R _ (extract_gen e1 b_in1) (extract_gen e2 b_in2).
+      Proof using abstract_interp_ident_Proper.
+        cbv [extract_gen].
+        eapply type.related_iff_app_curried; try assumption.
+        unshelve eapply expr.wf_interp_Proper_gen1; try eassumption.
+
+      Qed.
+
+      Lemma interp_extract_gen_from_wf
+        {t} (e1 e2 : expr t) b_in1 b_in2
+        (Hwf : expr.wf nil e1 e2)
+        (Hb_in : type.and_for_each_lhs_of_arrow (@abstract_domain_R) b_in1 b_in2)
+        : abstract_domain'_R _ (extract_gen e1 b_in1) (extract_gen e2 b_in2).
+      Proof using abstract_interp_ident_Proper.
+        eapply interp_extract_gen_from_wf_gen; try eassumption; wf_t.
       Qed.
 
       Context (interp_ident_Proper
                : forall annotate_with_state t idc,
-                  related_bounded_value (ident_extract t idc) (UnderLets.interp ident_interp (interp_ident annotate_with_state t idc)) (ident_interp t idc)).
+                  related_bounded_value (interp_ident annotate_with_state idc) (ident_interp t idc)).
 
       Lemma interp_interp
-            annotate_with_state G G' {t} (e_st e1 e2 e3 : expr t)
-            (HG : forall t v1 v2 v3, List.In (existT _ t (v1, v2, v3)) G
-                                     -> related_bounded_value_with_lets v1 v2 v3)
-            (HG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> v1 == v2)
-            (Hwf : expr.wf3 G e_st e1 e2)
-            (Hwf' : expr.wf G' e2 e3)
-        : related_bounded_value_with_lets
-            (extract' e_st)
-            (interp annotate_with_state e1)
-            (expr.interp (@ident_interp) e2).
-      Proof using interp_ident_Proper interp_annotate abstraction_relation'_Proper ident_interp_Proper' abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_Proper bottom'_related.
-        clear -ident_interp_Proper' interp_ident_Proper interp_annotate abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_Proper bottom'_related HG HG' Hwf Hwf'.
-        cbv [related_bounded_value_with_lets] in *;
-          revert dependent annotate_with_state; revert dependent G'; induction Hwf; intros;
-            cbn [extract' interp expr.interp UnderLets.interp List.In related_bounded_value reify reflect] in *; cbv [Let_In] in *.
+        annotate_with_state G G' G'' G''' {t} (e e_st e_v : expr t)
+        (HG : forall t v1 v2 v3, List.In (existT _ t (v1, v2, v3)) G
+                                 -> related_bounded_value v2 v3
+                                    /\ abstract_domain_R v1 (state_of_value v2))
+        (HG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G' -> abstract_domain_R (state_of_value v1) v2)
+        (HG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G'' -> v1 == v2)
+        (HG''' : forall t v1 v2, List.In (existT _ t (v1, v2)) G''' -> abstract_domain_R v1 v2)
+        (Hwf : expr.wf3 G e_st e e_v)
+        (Hwf' : expr.wf G' e e_st)
+        (Hwf'' : expr.wf G'' e_v e_v)
+        (Hwf''' : expr.wf G''' e_st e_st)
+        : related_bounded_value
+            (interp annotate_with_state e e_st)
+            (expr.interp (@ident_interp) e_v)
+          /\ abstract_domain_R (expr.interp (@abstract_interp_ident) e_st) (state_of_value (interp annotate_with_state e e_st)).
+      Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstraction_relation'_Proper ident_interp_Proper' interp_annotate interp_ident_Proper try_make_transport_base_type_cps_correct.
+        clear -abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstraction_relation'_Proper ident_interp_Proper' interp_annotate interp_ident_Proper try_make_transport_base_type_cps_correct HG HG' HG'' HG''' Hwf Hwf' Hwf'' Hwf'''.
+        cbv [related_bounded_value] in *;
+          revert dependent annotate_with_state; revert dependent G'; revert dependent G''; revert dependent G'''; induction Hwf; intros.
         all: destruct annotate_with_state eqn:?.
+        all: cbn [interp expr.interp UnderLets.interp List.In related_bounded_value' reify reflect abstract_domain_R type.related] in *; cbv [Let_In Proper respectful] in *; cbn [state_of_value Base_value' fst snd] in *.
+        all: repeat apply conj; intros.
         all: repeat first [ progress intros
                           | progress subst
                           | progress inversion_sigma
-                          | progress inversion_prod
-                          | progress destruct_head'_and
-                          | progress destruct_head'_or
+                          | progress inversion_pair
                           | progress destruct_head'_sig
-                          | progress destruct_head'_sigT
-                          | progress destruct_head'_prod
+                          | progress destruct_head'_and
                           | progress eta_expand
-                          | exfalso; assumption
-                          | progress cbn [UnderLets.interp List.In eq_rect fst snd projT1 projT2] in *
+                          | progress cbv [interp_ident] in *
+                          | progress cbn [eq_rect UnderLets.interp project_value' state_of_value fst snd Base_value' List.In apply_value] in *
+                          | progress eliminate_hprop_eq
+                          | apply related_bounded_value_annotate_base
+                          | eapply abstract_domain_R_of_related_bounded_value'; eassumption
+                          | eapply related_of_related_bounded_value'; eassumption
+                          | solve [ cbv [abstract_domain_R] in *; (idtac + symmetry); eauto ]
+                          | progress split_and
+                          | erewrite invert_default_Some by reflexivity
+                          | erewrite invert_default'_Some by reflexivity
                           | rewrite UnderLets.interp_splice
-                          | rewrite interp_annotate
-                          | solve [ cbv [Proper respectful Basics.impl] in *; unshelve eauto using related_of_related_bounded_value, related_bounded_value_bottomify ]
-                          | progress specialize_by_assumption
-                          | progress cbv [Let_In] in *
-                          | progress cbn [state_of_value extract'] in *
-                          | progress expr.invert_subst
-                          | match goal with
-                            | [ |- abstract_domain ?t ] => exact (@bottom t)
-                            | [ H : expr.wf _ _ _ |- Proper type.eqv _ ]
-                              => apply expr.wf_interp_Proper_gen1 in H;
-                                 [ cbv [Proper]; etransitivity; (idtac + symmetry); exact H | auto ]
-                            | [ H : _ |- _ ]
-                              => (tryif first [ constr_eq H HG | constr_eq H HG' ]
-                                   then fail
-                                   else (apply H; clear H))
-                            | [ |- related_bounded_value _ (fst _, UnderLets.interp _ (annotate _ _ _ _)) _ ]
-                              => apply related_bounded_value_annotate_base
-                            | [ H : context[match ?v with None => _ | _ => _ end] |- _ ] => destruct v eqn:?
-                            | [ H : context[@related_bounded_value (type.base ?t) ?x _ ?y]
-                                |- @related_bounded_value (type.base ?t) ?x _ ?y ]
-                              => eapply related_bounded_value_Proper_interp_eq_base; [ reflexivity | split; hnf | reflexivity | eapply H ];
-                                 cbn [fst snd expr.interp];
-                                 [ reflexivity | reflexivity | .. ]
-                            end
-                          | apply conj
+                          | progress destruct_head'_or
+                          | eapply expr.wf_interp_Proper_gen1; [ | now eauto ]
                           | match goal with
-                            | [ H : _ = _ |- _ ] => rewrite H
+                            | [ |- _ /\ _ ] => split
                             end
-                          | break_innermost_match_step
-                          | progress expr.inversion_wf_one_constr
+                          | progress expr.inversion_wf_constr
+                          | do_with_hyp' ltac:(fun H => now apply H; first [ eapply related_of_related_bounded_value' | eapply related_refl_of_related_bounded_value' ]; eauto)
                           | match goal with
-                            | [ H : _ |- _ ]
-                              => (tryif first [ constr_eq H HG | constr_eq H HG' ]
-                                   then fail
-                                   else (eapply H; clear H;
-                                         [ lazymatch goal with
-                                           | [ |- expr.wf _ _ _ ]
-                                             => solve [ eassumption
-                                                      | match goal with
-                                                        | [ H : forall v1 v2, expr.wf _ _ _ |- expr.wf _ (?f ?x) _ ]
-                                                          => apply (H x x)
-                                                        end ]
-                                           | [ |- bool ] (* unused [annotate_with_state] argument to a [Proper ... /\ ...] lemma which is used for its [Proper] part *)
-                                             => constructor
-                                           | _ => idtac
-                                           end .. ];
-                                         match goal with
-                                           [ |- ?G ] => assert_fails has_evar G
-                                         end))
+                            | [ H : context[related_bounded_value' _ (UnderLets.interp _ (project_value' (interp _ (?f2 _) (?f1 _)))) (expr.interp _ (?f3 _))]
+                                |- related_bounded_value' _ (UnderLets.interp _ (project_value' (interp _ (?f2 _) (?f1 _)))) (expr.interp _ (?f3 _)) ]
+                              => first [ eapply H
+                                       | eapply related_bounded_value'_Proper1; [ | reflexivity .. | eapply H ] ];
+                                 lazymatch goal with
+                                 | [ |- expr.wf _ _ _ ] => solve [ eauto ]
+                                 | _ => idtac
+                                 end;
+                                 clear H
+                            | [ H : context[related_bounded_value' _ (UnderLets.interp _ (UnderLets.interp _ (project_value' (interp _ ?f2 ?f1)) _)) (expr.interp _ ?f3 _)]
+                                |- related_bounded_value' _ (UnderLets.interp _ (UnderLets.interp _ (project_value' (interp _ ?f2 ?f1)) _)) (expr.interp _ ?f3 _) ]
+                              => first [ eapply H
+                                       | eapply related_bounded_value'_Proper1; [ | reflexivity .. | eapply H ] ];
+                                 lazymatch goal with
+                                 | [ |- expr.wf _ _ _ ] => solve [ eauto ]
+                                 | _ => idtac
+                                 end;
+                                 clear H
+                            | [ H : context[abstract_domain_R (expr.interp _ (?f1 _)) (state_of_value (interp _ (?f2 _) (?f1 _)))]
+                                |- abstract_domain_R (expr.interp _ (?f1 _)) (state_of_value (interp _ (?f2 _) (?f1 _))) ]
+                              => first [ eapply H; clear H
+                                       | etransitivity; [ | eapply H; clear H ] ];
+                                 lazymatch goal with
+                                 | [ |- expr.wf _ _ _ ] => solve [ eauto ]
+                                 | _ => idtac
+                                 end
+                            | [ H : context[type.related abstract_domain'_R (expr.interp _ ?f1 _) (state_of_value (interp _ ?f2 ?f1) _)]
+                                |- abstract_domain_R (expr.interp _ ?f1 _) (state_of_value (interp _ ?f2 ?f1) _) ]
+                              => eapply H; clear H;
+                                 lazymatch goal with
+                                 | [ |- expr.wf _ _ _ ] => solve [ eauto ]
+                                 | _ => idtac
+                                 end
+                            | [ H : context[_ -> abstract_domain_R _ (state_of_value (interp _ ?f _))]
+                                |- abstract_domain_R (state_of_value (interp _ ?f ?x)) (state_of_value (interp _ ?f ?x)) ]
+                              => etransitivity; [ symmetry | ]; eapply H; clear H;
+                                 lazymatch goal with
+                                 | [ |- expr.wf _ _ _ ] => solve [ eauto ]
+                                 | _ => idtac
+                                 end
+                            | [ |- abstract_domain_R (state_of_value _) (expr.interp _ _) ] => symmetry
                             end
-                          | reflexivity ].
+                          | progress repeat first [ progress eta_expand | break_innermost_match_step ] ].
       Qed.
 
       Lemma interp_eval_with_bound'
-            annotate_with_state {t} (e_st e1 e2 : expr t)
-            (Hwf : expr.wf3 nil e_st e1 e2)
-            (Hwf' : expr.wf nil e2 e2)
-            (Ht : type.is_not_higher_order t = true)
+            annotate_with_state {t} (e e_st e_v : expr t)
+            (Hwf : expr.wf3 nil e_st e e_v)
+            (Hwf' : expr.wf nil e e_st)
+            (Hwf'' : expr.wf nil e_v e_v)
+            (Hwf''' : expr.wf nil e_st e_st)
             (st : type.for_each_lhs_of_arrow abstract_domain t)
-            (Hst : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) st)
         : (forall arg1 arg2
                   (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
                   (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1),
-              type.app_curried (expr.interp ident_interp (eval_with_bound' annotate_with_state e1 st)) arg1
-              = type.app_curried (expr.interp ident_interp e2) arg2)
+              type.app_curried (expr.interp ident_interp (eval_with_bound' annotate_with_state e e_st st)) arg1
+              = type.app_curried (expr.interp ident_interp e_v) arg2)
           /\ (forall arg1
                      (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1)
                      (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1),
                  abstraction_relation'
                    _
                    (extract_gen e_st st)
-                   (type.app_curried (expr.interp ident_interp (eval_with_bound' annotate_with_state e1 st)) arg1)).
-      Proof using interp_annotate abstraction_relation'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric bottom'_related interp_ident_Proper bottom'_Proper ident_interp_Proper'.
-        cbv [extract_gen extract' eval_with_bound'].
-        split; intros; rewrite UnderLets.interp_to_expr, UnderLets.interp_splice.
-        all: eapply interp_reify_first_order; eauto.
-        all: eapply interp_interp; eauto; wf_t.
+                   (type.app_curried (expr.interp ident_interp (eval_with_bound' annotate_with_state e e_st st)) arg1)).
+      Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstraction_relation'_Proper bottom'_Proper bottom'_related ident_interp_Proper' interp_annotate interp_ident_Proper try_make_transport_base_type_cps_correct.
+        cbv [extract_gen eval_with_bound'].
+        split; intros; rewrite UnderLets.interp_to_expr.
+        { apply interp_reify; eauto; [].
+          eapply interp_interp; eauto; wf_t. }
+        { erewrite interp_reify; try eassumption.
+          { eapply abstraction_relation_of_related_bounded_value'_app_curried; try assumption; [].
+            eapply related_bounded_value'_Proper1; [ .. | eapply interp_interp ]; try reflexivity; try eassumption; eauto; wf_t; [].
+            symmetry; eapply interp_interp; try eassumption; wf_t. }
+          { now eapply interp_interp; eauto; wf_t. } }
+        Unshelve.
+        all: exact true.
       Qed.
 
       Lemma interp_eta_expand_with_bound'
@@ -664,38 +703,12 @@ Module Compilers.
             (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
             (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1),
           type.app_curried (expr.interp ident_interp (eta_expand_with_bound' e1 b_in)) arg1 = type.app_curried (expr.interp ident_interp e2) arg2.
-      Proof using interp_annotate ident_interp_Proper' bottom'_related abstraction_relation'_Proper bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric.
+      Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstraction_relation'_Proper bottom'_Proper bottom'_related ident_interp_Proper' interp_annotate.
         cbv [eta_expand_with_bound'].
         intros; rewrite UnderLets.interp_to_expr.
         eapply interp_reify; eauto.
-        eapply interp_reflect; eauto using bottom_related.
-        eapply @expr.wf_interp_Proper_gen; auto using Hwf.
-      Qed.
-
-      Lemma interp_extract'_from_wf_gen G
-            (HG : forall t v1 v2, List.In (existT _ t (v1, v2)) G -> abstract_domain_R v1 v2)
-            {t} (e1 e2 : expr t)
-            (Hwf : expr.wf G e1 e2)
-        : abstract_domain_R (extract' e1) (extract' e2).
-      Proof using ident_extract_Proper bottom'_Proper.
-        cbv [abstract_domain_R] in *; induction Hwf; cbn [extract']; break_innermost_match.
-        all: repeat first [ progress subst
-                          | progress inversion_sigma
-                          | progress inversion_prod
-                          | solve [ cbv [Proper respectful] in *; eauto ]
-                          | progress cbv [respectful Let_In] in *
-                          | progress cbn [type.related List.In eq_rect partial.bottom] in *
-                          | progress intros
-                          | progress destruct_head'_or
-                          | apply bottom_Proper
-                          | match goal with H : _ |- type.related _ _ _ => apply H; clear H end ].
-      Qed.
-
-      Lemma interp_extract'_from_wf {t} (e1 e2 : expr t)
-            (Hwf : expr.wf nil e1 e2)
-        : abstract_domain_R (extract' e1) (extract' e2).
-      Proof using ident_extract_Proper bottom'_Proper.
-        eapply interp_extract'_from_wf_gen; revgoals; wf_t.
+        eapply interp_reflect; try (apply bottom_related; etransitivity; [ | symmetry ]).
+        all: eapply @expr.wf_interp_Proper_gen; [ | exact Hwf ]; auto.
       Qed.
     End with_type.
 
@@ -714,19 +727,20 @@ Module Compilers.
                 (extract_option_state : forall A, abstract_domain' (base.type.option A) -> option (option (abstract_domain' A)))
                 (is_annotated_for : forall t t', @expr var t -> abstract_domain' t' -> bool)
                 (skip_annotations_under : forall t, ident t -> bool)
-                (strip_annotation : forall t, ident t -> option (@value base.type ident var abstract_domain' t))
+                (strip_annotation : forall t, ident t -> option (@value' base.type ident var abstract_domain' t))
                 (abstraction_relation' : forall t, abstract_domain' t -> base.interp t -> Prop)
                 (abstract_domain'_R : forall t, abstract_domain' t -> abstract_domain' t -> Prop)
                 (abstraction_relation'_Proper : forall t, Proper (abstract_domain'_R t ==> eq ==> Basics.impl) (abstraction_relation' t))
                 (bottom'_related : forall t v, abstraction_relation' t (bottom' t) v)
                 {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)}
                 {abstract_domain'_R_transitive : forall t, Transitive (@abstract_domain'_R t)}
-                {abstract_domain'_R_symmetric : forall t, Symmetric (@abstract_domain'_R t)}.
-        Local Notation abstraction_relation := (@abstraction_relation base.type abstract_domain' base.interp abstraction_relation').
+                {abstract_domain'_R_symmetric : forall t, Symmetric (@abstract_domain'_R t)}
+                (abstract_domain'_R_of_related : forall t st v, @abstraction_relation' t st v -> @abstract_domain'_R t st st).
+        Local Notation abstraction_relation := (@abstraction_relation base.type abstract_domain' base.interp abstraction_relation' abstract_domain'_R).
         Local Notation ident_interp := ident.interp (only parsing).
         Local Notation abstract_domain_R := (@abstract_domain_R base.type abstract_domain' abstract_domain'_R).
-        Local Notation fill_in_bottom_for_arrows := (@fill_in_bottom_for_arrows base.type abstract_domain' bottom').
-        Local Notation related_bounded_value := (@related_bounded_value base.type ident abstract_domain' base.interp (@ident_interp) abstraction_relation' bottom' abstract_domain'_R).
+        Local Notation related_bounded_value' := (@related_bounded_value' base.type ident abstract_domain' base.interp (@ident_interp) abstraction_relation' abstract_domain'_R).
+        Local Notation related_bounded_value := (@related_bounded_value base.type ident abstract_domain' base.interp (@ident_interp) abstraction_relation' abstract_domain'_R).
         Context {abstract_interp_ident_Proper : forall t, Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t)}
                 (interp_annotate_expr
                  : forall t st idc,
@@ -734,7 +748,7 @@ Module Compilers.
                     -> forall v, abstraction_relation' _ st v
                            -> expr.interp (@ident_interp) idc v = v)
                 (abstract_interp_ident_Proper'
-                 : forall t idc, type.related_hetero (@abstraction_relation') (abstract_interp_ident t idc) (ident_interp idc))
+                 : forall t idc, abstraction_relation (abstract_interp_ident t idc) (ident_interp idc))
                 (extract_list_state_related
                  : forall t st ls v st' v',
                     extract_list_state t st = Some ls
@@ -754,7 +768,7 @@ Module Compilers.
                 (strip_annotation_related
                  : forall t idc v,
                     strip_annotation t idc = Some v
-                    -> related_bounded_value (abstract_interp_ident t idc) v (ident_interp idc)).
+                    -> related_bounded_value' (abstract_interp_ident t idc) v (ident_interp idc)).
 
         Local Notation update_annotation := (@ident.update_annotation _ abstract_domain' annotate_expr is_annotated_for).
         Local Notation annotate_with_expr := (@ident.annotate_with_expr _ abstract_domain' annotate_expr is_annotated_for).
@@ -763,18 +777,6 @@ Module Compilers.
         Local Notation reify := (@reify base.type ident _ abstract_domain' annotate bottom').
         Local Notation reflect := (@reflect base.type ident _ abstract_domain' annotate bottom').
 
-        Lemma abstract_interp_ident_Proper'' t idc
-          : type.related_hetero (@abstraction_relation') (fill_in_bottom_for_arrows (abstract_interp_ident t idc)) (ident_interp idc).
-        Proof using abstract_interp_ident_Proper' bottom'_related.
-          generalize (abstract_interp_ident_Proper' t idc); clear -bottom'_related.
-          generalize (ident_interp idc), (abstract_interp_ident t idc); clear idc.
-          intros v st H.
-          induction t as [| [|s' d'] IHs d IHd]; cbn in *; cbv [respectful_hetero] in *;
-            auto.
-          intros; apply IHd, H; clear IHd H.
-          intros; apply bottom_related; assumption.
-        Qed.
-
         Lemma interp_update_annotation t st e
               (He : abstraction_relation' t st (expr.interp (t:=type.base t) (@ident_interp) e))
           : expr.interp (@ident_interp) (@update_annotation t st e)
@@ -827,7 +829,7 @@ Module Compilers.
                             | progress break_innermost_match
                             | progress break_innermost_match_hyps
                             | progress expr.invert_subst
-                            | progress cbn [fst snd UnderLets.interp expr.interp ident_interp Nat.add] in *
+                            | progress cbn [fst snd UnderLets.interp expr.interp ident.interp Nat.add] in *
                             | progress cbv [ident.literal] in *
                             | match goal with
                               | [ H : context[ident_interp (ident.ident_Literal _)] |- _ ] => rewrite ident.interp_ident_Literal in H
@@ -846,9 +848,13 @@ Module Compilers.
                             | match goal with
                               | [ H : context[expr.interp _ (reify_list _)] |- _ ] => rewrite expr.interp_reify_list in H
                               | [ H : abstraction_relation' (_ * _) _ (_, _) |- _ ]
-                                => pose proof (abstract_interp_ident_Proper'' _ ident.fst _ _ H);
-                                  pose proof (abstract_interp_ident_Proper'' _ ident.snd _ _ H);
-                                  clear H
+                                => let H' := fresh in
+                                   let H'' := fresh in
+                                   pose proof H as H';
+                                   pose proof H as H'';
+                                   apply (abstract_interp_ident_Proper' _ ident.fst) in H';
+                                   apply (abstract_interp_ident_Proper' _ ident.snd) in H'';
+                                   clear H
                               | [ H : context[_ = _] |- _ = _ ] => rewrite H by assumption
                               | [ |- List.map ?f (List.combine ?l1 ?l2) = List.map ?g ?l2 ]
                                 => transitivity (List.map g (List.map (@snd _ _) (List.combine l1 l2)));
@@ -905,38 +911,43 @@ Module Compilers.
                               end ].
         Qed.
 
-        Local Notation interp_ident := (@ident.interp_ident _ abstract_domain' annotate_expr bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for strip_annotation).
+        Local Notation interp_ident' := (@ident.interp_ident' _ abstract_domain' annotate_expr bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for strip_annotation).
 
         Lemma interp_ident_Proper_not_nth_default_nostrip annotate_with_state t idc
-          : related_bounded_value (abstract_interp_ident t idc) (UnderLets.interp (@ident_interp) (Base (reflect annotate_with_state (expr.Ident idc) (abstract_interp_ident _ idc)))) (ident_interp idc).
-        Proof using abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr abstract_interp_ident_Proper bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric.
-          cbn [UnderLets.interp].
+          : related_bounded_value (reflect annotate_with_state (expr.Ident idc) (abstract_interp_ident _ idc)) (@ident_interp t idc).
+        Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr.
           eapply interp_reflect;
             try first [ apply ident.interp_Proper
-                      | apply abstract_interp_ident_Proper''
                       | eapply abstract_interp_ident_Proper; reflexivity
                       | apply interp_annotate ];
             eauto.
         Qed.
 
         Lemma interp_ident_Proper_not_nth_default annotate_with_state t idc
-          : related_bounded_value
+          : related_bounded_value'
               (abstract_interp_ident t idc)
-              ((UnderLets.interp (@ident_interp))
-                 (Base match strip_annotation _ idc with
-                       | Some v => v
-                       | None => reflect annotate_with_state (expr.Ident idc) (abstract_interp_ident _ idc)
-                       end))
+              (UnderLets.interp
+                 (@ident.interp)
+                 match strip_annotation _ idc with
+                 | Some v => Base v
+                 | None => project_value' _ (reflect annotate_with_state (expr.Ident idc) (abstract_interp_ident _ idc))
+                 end)
               (ident_interp idc).
-        Proof using abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr abstract_interp_ident_Proper bottom'_Proper abstract_domain'_R_transitive abstract_domain'_R_symmetric strip_annotation_related.
+        Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr strip_annotation_related.
           pose proof (strip_annotation_related t idc) as H.
+          cbv [related_bounded_value].
           break_innermost_match; eauto using eq_refl, interp_ident_Proper_not_nth_default_nostrip.
+          eapply related_bounded_value'_Proper1; [ try exact eq_refl; try exact _ .. | eapply interp_reflect; eauto using interp_annotate ].
+          all: eauto.
+          all: rewrite ?state_of_value_reflect.
+          all: try now apply abstract_interp_ident_Proper.
+          all: try now apply Compilers.eqv_Reflexive_Proper.
         Qed.
 
         Lemma interp_ident_Proper_nth_default annotate_with_state T (idc:=@ident.List_nth_default T)
-          : related_bounded_value (abstract_interp_ident _ idc) (UnderLets.interp (@ident_interp) (interp_ident annotate_with_state idc)) (ident_interp idc).
-        Proof using abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr bottom'_related.
-          subst idc; cbn [interp_ident reify reflect fst snd UnderLets.interp ident_interp related_bounded_value abstract_domain value].
+          : related_bounded_value' (abstract_interp_ident _ idc) (UnderLets.interp (@ident.interp) (interp_ident' annotate_with_state idc)) (ident_interp idc).
+        Proof using abstract_domain'_R_of_related abstract_interp_ident_Proper abstract_interp_ident_Proper' bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr.
+          subst idc; cbn [interp_ident reify reflect fst snd UnderLets.interp ident_interp related_bounded_value' abstract_domain value].
           cbv [abstract_domain]; cbn [type.interp bottom_for_each_lhs_of_arrow state_of_value fst snd].
           repeat first [ progress intros
                        | progress cbn [UnderLets.interp fst snd expr.interp ident_interp] in *
@@ -952,7 +963,7 @@ Module Compilers.
                        | solve [ cbv [Proper respectful Basics.impl] in *; eauto ]
                        | split; [ apply (@abstract_interp_ident_Proper _ (@ident.List_nth_default T) _ eq_refl) | ]
                        | split; [ reflexivity | ]
-                       | apply (@abstract_interp_ident_Proper'' _ (@ident.List_nth_default T))
+                       | apply (@abstract_interp_ident_Proper' _ (@ident.List_nth_default T))
                        | apply conj
                        | rewrite map_nth_default_always
                        | rewrite expr.interp_reify_list
@@ -964,53 +975,58 @@ Module Compilers.
                          | [ H : _ = reify_list _ |- _ ] => apply (f_equal (expr.interp (@ident_interp))) in H
                          | [ H : expr.interp _ ?x = _ |- context[expr.interp _ ?x] ] => rewrite H
                          | [ |- Proper _ _ ] => cbv [Proper type.related respectful]
-                         end ].
+                         end
+                       | progress cbn [interp_ident' reify snd fst Base_value' reflect project_value']; eta_expand ].
         Qed.
 
         Lemma interp_ident_Proper annotate_with_state t idc
-          : related_bounded_value (abstract_interp_ident t idc) (UnderLets.interp (@ident_interp) (interp_ident annotate_with_state idc)) (ident_interp idc).
-        Proof using abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr strip_annotation_related.
+          : related_bounded_value' (abstract_interp_ident _ idc) (UnderLets.interp (@ident.interp) (@interp_ident' t annotate_with_state idc)) (ident_interp idc).
+        Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr strip_annotation_related.
           pose idc as idc'.
-          destruct idc; first [ refine (@interp_ident_Proper_not_nth_default _ _ idc')
-                              | refine (@interp_ident_Proper_nth_default _ _) ].
+          destruct idc;
+            first [ refine (@interp_ident_Proper_not_nth_default _ _ idc')
+                  | refine (@interp_ident_Proper_nth_default _ _) ].
         Qed.
 
         Local Notation eval_with_bound := (@partial.ident.eval_with_bound _ abstract_domain' annotate_expr bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for strip_annotation).
         Local Notation eta_expand_with_bound := (@partial.ident.eta_expand_with_bound _ abstract_domain' annotate_expr bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for).
-        Local Notation extract := (@ident.extract abstract_domain' bottom' abstract_interp_ident).
+        Local Notation extract := (@ident.extract abstract_domain' abstract_interp_ident).
 
         Lemma interp_eval_with_bound
-              annotate_with_state {t} (e_st e1 e2 : expr t)
-              (Hwf : expr.wf3 nil e_st e1 e2)
-              (Hwf' : expr.wf nil e2 e2)
-              (Ht : type.is_not_higher_order t = true)
-              (st : type.for_each_lhs_of_arrow abstract_domain t)
-              (Hst : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) st)
+          annotate_with_state {t} (e e_st e_v : expr t)
+          (Hwf : expr.wf3 nil e_st e e_v)
+          (Hwf' : expr.wf nil e e_st)
+          (Hwf'' : expr.wf nil e_v e_v)
+          (Hwf''' : expr.wf nil e_st e_st)
+          (st : type.for_each_lhs_of_arrow abstract_domain t)
           : (forall arg1 arg2
                     (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
                     (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1),
-                type.app_curried (expr.interp (@ident_interp) (eval_with_bound skip_annotations_under annotate_with_state e1 st)) arg1
-                = type.app_curried (expr.interp (@ident_interp) e2) arg2)
+                type.app_curried (expr.interp (@ident_interp) (eval_with_bound skip_annotations_under annotate_with_state e e_st st)) arg1
+                = type.app_curried (expr.interp (@ident_interp) e_v) arg2)
             /\ (forall arg1
                        (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) st arg1)
                        (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1),
                    abstraction_relation'
                      _
                      (extract e_st st)
-                     (type.app_curried (expr.interp (@ident_interp) (eval_with_bound skip_annotations_under annotate_with_state e1 st)) arg1)).
-        Proof using abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr strip_annotation_related. cbv [extract eval_with_bound]; apply @interp_eval_with_bound' with (abstract_domain'_R:=abstract_domain'_R); auto using interp_annotate, interp_ident_Proper, ident.interp_Proper. Qed.
+                     (type.app_curried (expr.interp (@ident_interp) (eval_with_bound skip_annotations_under annotate_with_state e e_st st)) arg1)).
+        Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr strip_annotation_related.
+          cbv [extract eval_with_bound]; eapply @interp_eval_with_bound' with (abstract_domain'_R:=abstract_domain'_R); auto using interp_annotate, interp_ident_Proper, ident.interp_Proper; try exact _; intros; apply interp_ident_Proper.
+        Qed.
 
         Lemma interp_eta_expand_with_bound
               {t} (e1 e2 : expr t)
               (Hwf : expr.wf nil e1 e2)
-              (Ht : type.is_not_higher_order t = true)
               (b_in : type.for_each_lhs_of_arrow abstract_domain t)
               (Hb_in : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) b_in)
           : forall arg1 arg2
                    (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
                    (Harg1 : type.and_for_each_lhs_of_arrow (@abstraction_relation) b_in arg1),
             type.app_curried (expr.interp (@ident_interp) (eta_expand_with_bound e1 b_in)) arg1 = type.app_curried (expr.interp (@ident_interp) e2) arg2.
-        Proof using abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr. cbv [partial.ident.eta_expand_with_bound]; eapply interp_eta_expand_with_bound'; eauto using interp_annotate, ident.interp_Proper. Qed.
+        Proof using abstract_domain'_R_of_related abstract_domain'_R_symmetric abstract_domain'_R_transitive abstract_interp_ident_Proper' abstraction_relation'_Proper bottom'_Proper bottom'_related extract_list_state_length_good extract_list_state_related extract_option_state_related interp_annotate_expr.
+          cbv [partial.ident.eta_expand_with_bound]; eapply interp_eta_expand_with_bound'; eauto using (@interp_ident), interp_annotate, ident.interp_Proper; try typeclasses eauto.
+        Qed.
       End with_type.
     End ident.
 
@@ -1028,11 +1044,12 @@ Module Compilers.
       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)).
-      Local Notation fill_in_bottom_for_arrows := (@fill_in_bottom_for_arrows base.type abstract_domain' bottom').
 
       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.
 
+      Local Notation abstraction_relation := (@abstraction_relation _ abstract_domain' _ (@abstraction_relation') (fun t => abstract_domain'_R t)).
+
       Lemma bottom'_bottom {t} : forall v, abstraction_relation' (bottom' t) v.
       Proof using Type.
         cbv [abstraction_relation' bottom']; induction t; cbn; intros; break_innermost_match; cbn; try reflexivity.
@@ -1040,8 +1057,8 @@ Module Compilers.
       Qed.
 
       Lemma abstract_interp_ident_related {opts : AbstractInterpretation.Options} {assume_cast_truncates : bool} {t} (idc : ident t)
-        : type.related_hetero (@abstraction_relation') (abstract_interp_ident assume_cast_truncates t idc) (ident.interp idc).
-      Proof using Type. apply ZRange.ident.option.interp_related. Qed.
+        : abstraction_relation (abstract_interp_ident assume_cast_truncates t idc) (ident.interp idc).
+      Proof using Type. apply ZRange.ident.option.interp_related_and_Proper. Qed.
 
       Local Ltac zrange_interp_idempotent_t :=
         repeat first [ progress destruct_head'_ex
@@ -1082,22 +1099,24 @@ Module Compilers.
         : ZRange.type.base.option.is_bounded_by (t:=base.type.Z*base.type.Z) (ZRange.ident.option.interp assume_cast_truncates ident.Z_cast2 r1 r2) v = true.
       Proof using Type. destruct r1, r2, assume_cast_truncates; zrange_interp_idempotent_t. Qed.
 
-      Local Notation related_bounded_value := (@related_bounded_value base.type ident abstract_domain' base.interp (@ident.interp) (@abstraction_relation') bottom' (fun t => abstract_domain'_R t)).
+      Local Notation related_bounded_value' := (@related_bounded_value' base.type ident abstract_domain' base.interp (@ident.interp) (@abstraction_relation') (fun t => abstract_domain'_R t)).
       Lemma always_strip_annotation_related {opts : AbstractInterpretation.Options} {assume_cast_truncates : bool} {t} (idc : ident t)
             v (Hv : always_strip_annotation assume_cast_truncates t idc = Some v)
-        : related_bounded_value (abstract_interp_ident assume_cast_truncates t idc) v (ident.interp idc).
+        : related_bounded_value' (abstract_interp_ident assume_cast_truncates t idc) v (ident.interp idc).
       Proof using Type.
         pose proof (@abstract_interp_ident_related _ assume_cast_truncates _ ident.Z_cast).
-        pose proof (fun x1 x2 y1 y2 H x01 x02 y01 y02 H' => @abstract_interp_ident_related _ assume_cast_truncates _ ident.Z_cast2 (x1, x2) (y1, y2) H (x01, x02) (y01, y02) H').
+        pose proof (fun x1 x2 y1 y2 H x01 x02 y01 y02 H' => proj2 (proj2 (proj2 (proj2 (@abstract_interp_ident_related _ assume_cast_truncates _ ident.Z_cast2)) (x1, x2) (y1, y2) H)) (x01, x02) (y01, y02) H').
+        cbn [abstraction_relation] in *.
         cbv [always_strip_annotation] in *; break_innermost_match_hyps; inversion_option; subst.
         all: repeat first [ reflexivity
-                          | progress cbn [related_bounded_value UnderLets.interp fst snd type.related_hetero] in *
+                          | progress cbn [related_bounded_value' UnderLets.interp fst snd type.related_hetero] in *
                           | progress cbv [respectful_hetero] in *
                           | progress intros
                           | progress destruct_head'_and
                           | progress subst
                           | progress inversion_prod
                           | progress inversion_option
+                          | progress destruct_head_hnf' prod
                           | match goal with
                             | [ |- Proper _ _ ] => exact _
                             | [ |- _ /\ _ ] => split
@@ -1117,7 +1136,7 @@ Module Compilers.
                           | progress break_innermost_match_hyps
                           | progress Reflect.reflect_beq_to_eq zrange_beq
                           | progress cbv [abstraction_relation' ZRange.type.base.option.lift_Some] in *
-                          | cbn [Compilers.ident_interp]; progress cbv [ident.cast2]
+                          | cbn [ident.interp]; progress cbv [ident.cast2]
                           | rewrite ident.cast_in_bounds by assumption
                           | now destruct assume_cast_truncates
                           | rewrite zrange_interp_idempotent_Z_cast by (cbn; eexists; eassumption)
@@ -1141,7 +1160,7 @@ Module Compilers.
 
       Lemma strip_annotation_related {opts : AbstractInterpretation.Options} {assume_cast_truncates strip_annotations : bool} {t} (idc : ident t)
             v (Hv : strip_annotation assume_cast_truncates strip_annotations t idc = Some v)
-        : related_bounded_value (abstract_interp_ident assume_cast_truncates t idc) v (ident.interp idc).
+        : related_bounded_value' (abstract_interp_ident assume_cast_truncates t idc) v (ident.interp idc).
       Proof using Type.
         destruct strip_annotations; cbv [strip_annotation] in *; try congruence;
           now apply always_strip_annotation_related.
@@ -1179,8 +1198,8 @@ Module Compilers.
         cbv [partial.Extract partial.ident.extract partial.extract_gen].
         revert b_in1 b_in2 Hb.
         rewrite <- (@type.related_iff_app_curried base.type ZRange.type.base.option.interp (fun _ => eq)).
-        apply interp_extract'_from_wf; auto with wf typeclass_instances.
-        apply GeneralizeVar.wf_from_flat_to_flat, Hwf.
+        eapply expr.wf_interp_Proper_gen1; [ | apply GeneralizeVar.wf_from_flat_to_flat, Hwf ].
+        wf_t.
       Qed.
 
       Lemma Extract_FromFlat_ToFlat {opts : AbstractInterpretation.Options} {assume_cast_truncates : bool} {t} (e : Expr t) (Hwf : Wf e) b_in
@@ -1244,35 +1263,35 @@ Module Compilers.
               {assume_cast_truncates : bool}
               {skip_annotations_under : forall t, ident t -> bool}
               {strip_preexisting_annotations : bool}
-              {t} (e_st e1 e2 : expr t)
-              (Hwf : expr.wf3 nil e_st e1 e2)
-              (Hwf' : expr.wf nil e2 e2)
-              (Ht : type.is_not_higher_order t = true)
+              {t} (e_st e e_v : expr t)
+              (Hwf : expr.wf3 nil e_st e e_v)
+              (Hwf' : expr.wf nil e e_st)
+              (Hwf'' : expr.wf nil e_v e_v)
+              (Hwf''' : expr.wf nil e_st e_st)
               (st : type.for_each_lhs_of_arrow abstract_domain 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) st arg1 = true),
-                type.app_curried (expr.interp (@ident.interp) (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e1 st)) arg1
-                = type.app_curried (expr.interp (@ident.interp) e2) arg2)
+                type.app_curried (expr.interp (@ident.interp) (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e e_st st)) arg1
+                = type.app_curried (expr.interp (@ident.interp) e_v) arg2)
             /\ (forall arg1
                        (Harg11 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg1)
                        (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
                    abstraction_relation'
                      (extract assume_cast_truncates e_st st)
-                     (type.app_curried (expr.interp (@ident.interp) (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e1 st)) arg1)).
+                     (type.app_curried (expr.interp (@ident.interp) (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e e_st st)) arg1)).
         Proof using Hrelax.
           cbv [eval_with_bound]; split;
             [ intros arg1 arg2 Harg12 Harg1
             | intros arg1 Harg11 Harg1 ].
-          all: eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1; [ | apply ZRange.type.option.is_bounded_by_impl_related_hetero ].
+          all: eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1; [ | apply @ZRange.type.option.is_bounded_by_impl_related_hetero_and_Proper with (skip_base:=true) ].
           all: eapply ident.interp_eval_with_bound with (abstraction_relation':=@abstraction_relation') (abstract_domain'_R:=fun t => abstract_domain'_R t); eauto using bottom'_bottom, interp_annotate_expr with typeclass_instances.
-          all: intros; (eapply extract_list_state_related + eapply extract_option_state_related + eapply strip_annotation_related); eassumption.
+          all: try (intros; (eapply extract_list_state_related + eapply extract_option_state_related + eapply strip_annotation_related); eassumption).
         Qed.
 
         Lemma interp_eta_expand_with_bound
               {t} (e1 e2 : expr t)
               (Hwf : expr.wf nil e1 e2)
-              (Ht : type.is_not_higher_order t = true)
               (b_in : type.for_each_lhs_of_arrow abstract_domain t)
           : forall arg1 arg2
                    (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
@@ -1282,8 +1301,9 @@ Module Compilers.
           cbv [partial.eta_expand_with_bound]; intros arg1 arg2 Harg12 Harg1.
           eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1.
           { apply ident.interp_eta_expand_with_bound with (abstraction_relation':=@abstraction_relation') (abstract_domain'_R:=fun t => abstract_domain'_R t); eauto using bottom'_bottom, interp_annotate_expr with typeclass_instances.
-            all: intros; (eapply extract_list_state_related + eapply extract_option_state_related); eassumption. }
-          { apply ZRange.type.option.is_bounded_by_impl_related_hetero. }
+            all: try (intros; (eapply extract_list_state_related + eapply extract_option_state_related); eassumption).
+            all: try (cbv [Proper]; eapply abstract_domain_R_refl_of_abstraction_relation_for_each_lhs_of_arrow; try eassumption; reflexivity). }
+          { apply ZRange.type.option.is_bounded_by_impl_related_hetero_and_Proper. }
         Qed.
 
         Lemma Interp_EvalWithBound
@@ -1293,9 +1313,7 @@ Module Compilers.
               {strip_preexisting_annotations : bool}
               {t} (e : Expr t)
               (Hwf : expr.Wf e)
-              (Ht : type.is_not_higher_order t = true)
               (st : type.for_each_lhs_of_arrow abstract_domain t)
-              (Hst : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) st)
           : (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) st arg1 = true),
@@ -1307,12 +1325,37 @@ Module Compilers.
                    abstraction_relation'
                      (Extract assume_cast_truncates e st)
                      (type.app_curried (expr.Interp (@ident.interp) (EvalWithBound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e st)) arg1)).
-        Proof using Hrelax. cbv [Extract EvalWithBound]; apply interp_eval_with_bound; try apply expr.Wf3_of_Wf; auto. Qed.
+        Proof using Hrelax.
+          cbv [EvalWithBound Let_In].
+          epose proof (interp_eval_with_bound
+                         (GeneralizeVar.FromFlat (GeneralizeVar.ToFlat e) _)
+                         (GeneralizeVar.FromFlat (GeneralizeVar.ToFlat e) _)
+                         (GeneralizeVar.FromFlat (GeneralizeVar.ToFlat e) _)) as H.
+          edestruct H as [H0 H1]; [ shelve .. | ].
+          split; intros.
+          { cbv [expr.Interp]; erewrite H0 by eassumption.
+            eapply (@type.related_iff_app_curried _ _ (fun _ => eq) t).
+            { apply GeneralizeVar.Interp_gen1_FromFlat_ToFlat; eauto. }
+            { etransitivity; (idtac + symmetry); eassumption. } }
+          { lazymatch goal with
+            | [ H : context[abstraction_relation' ?e _] |- abstraction_relation' ?e' _ ]
+              => replace e' with e; [ now eapply H | ]
+            end.
+            apply Extract_FromFlat_ToFlat'; eauto; [].
+            eapply type.and_for_each_lhs_of_arrow_Proper_impl_hetero1;
+              [ | eapply type.andb_bool_impl_and_for_each_lhs_of_arrow; [ | eassumption ] ];
+              [ | refine (fun t x y H => H) ];
+              cbv beta.
+            intros *; eapply ZRange.type.option.is_bounded_by_impl_eqv_refl. }
+          Unshelve.
+          all: try apply expr.Wf3_of_Wf.
+          all: apply GeneralizeVar.Wf_FromFlat_to_flat.
+          all: apply Hwf.
+        Qed.
 
         Lemma Interp_EtaExpandWithBound
               {t} (E : Expr t)
               (Hwf : Wf E)
-              (Ht : type.is_not_higher_order t = true)
               (b_in : type.for_each_lhs_of_arrow abstract_domain t)
           : forall arg1 arg2
                    (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
@@ -1367,29 +1410,30 @@ Module Compilers.
       Lemma interp_strip_annotations
             {opts : AbstractInterpretation.Options}
             {assume_cast_truncates : bool}
-            {t} (e_st e1 e2 : expr t)
-            (Hwf : expr.wf3 nil e_st e1 e2)
-            (Hwf' : expr.wf nil e2 e2)
-            (Ht : type.is_not_higher_order t = true)
+            {t} (e_st e e_v : expr t)
+            (Hwf : expr.wf3 nil e_st e e_v)
+            (Hwf' : expr.wf nil e e_st)
+            (Hwf'' : expr.wf nil e_v e_v)
+            (Hwf''' : expr.wf nil e_st e_st)
             (st : type.for_each_lhs_of_arrow abstract_domain 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) st arg1 = true),
-              type.app_curried (expr.interp (@ident.interp) (strip_annotations assume_cast_truncates e1 st)) arg1
-              = type.app_curried (expr.interp (@ident.interp) e2) arg2)
+              type.app_curried (expr.interp (@ident.interp) (strip_annotations assume_cast_truncates e e_st st)) arg1
+              = type.app_curried (expr.interp (@ident.interp) e_v) arg2)
           /\ (forall arg1
                      (Harg11 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg1)
                      (Harg1 : type.andb_bool_for_each_lhs_of_arrow (@ZRange.type.option.is_bounded_by) st arg1 = true),
                  abstraction_relation'
                    (extract assume_cast_truncates e_st st)
-                   (type.app_curried (expr.interp (@ident.interp) (strip_annotations assume_cast_truncates e1 st)) arg1)).
+                   (type.app_curried (expr.interp (@ident.interp) (strip_annotations assume_cast_truncates e e_st st)) arg1)).
       Proof using Type.
         cbv [strip_annotations]; split;
           [ intros arg1 arg2 Harg12 Harg1
           | intros arg1 Harg11 Harg1 ].
-        all: eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1; [ | apply ZRange.type.option.is_bounded_by_impl_related_hetero ].
+        all: eapply Compilers.type.andb_bool_impl_and_for_each_lhs_of_arrow in Harg1; [ | apply @ZRange.type.option.is_bounded_by_impl_related_hetero_and_Proper with (skip_base:=true) ].
         all: eapply ident.interp_eval_with_bound with (abstraction_relation':=@abstraction_relation') (abstract_domain'_R:=fun t => abstract_domain'_R t); eauto using bottom'_bottom, interp_annotate_expr, default_relax_zrange_good, abstract_interp_ident_related with typeclass_instances.
-        all: intros; (eapply extract_list_state_related + eapply extract_option_state_related + eapply strip_annotation_related); eassumption.
+        all: try (intros; (eapply extract_list_state_related + eapply extract_option_state_related + eapply strip_annotation_related); eassumption).
       Qed.
 
       Lemma Interp_StripAnnotations
@@ -1397,7 +1441,6 @@ Module Compilers.
             {assume_cast_truncates : bool}
             {t} (E : Expr t)
             (Hwf : Wf E)
-            (Ht : type.is_not_higher_order t = true)
             (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)
@@ -1413,7 +1456,6 @@ Module Compilers.
             {assume_cast_truncates : bool}
             {t} (E : Expr t)
             (Hwf : expr.Wf E)
-            (Ht : type.is_not_higher_order t = true)
             (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
         : forall arg1
                  (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1)
@@ -1429,7 +1471,6 @@ Module Compilers.
       Lemma Interp_EtaExpandWithListInfoFromBound
             {t} (E : Expr t)
             (Hwf : Wf E)
-            (Ht : type.is_not_higher_order t = true)
             (b_in : type.for_each_lhs_of_arrow abstract_domain t)
         : forall arg1 arg2
                  (Harg12 : type.and_for_each_lhs_of_arrow (@type.eqv) arg1 arg2)
@@ -1453,7 +1494,6 @@ Module Compilers.
                                  -> is_tighter_than_bool z r' = true)
         {t} (E : Expr t)
         (Hwf : Wf E)
-        (Ht : type.is_not_higher_order t = true)
         (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)
@@ -1479,7 +1519,6 @@ Module Compilers.
                                  -> is_tighter_than_bool z r' = true)
         {t} (E : Expr t)
         (Hwf : Wf E)
-        (Ht : type.is_not_higher_order t = true)
         (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
     : forall arg1
              (Harg11 : Proper (type.and_for_each_lhs_of_arrow (@type.eqv)) arg1)
@@ -1491,15 +1530,20 @@ Module Compilers.
   Proof.
     cbv [PartialEvaluateWithBounds].
     intros arg1 Harg11 Harg1.
-    rewrite <- Extract_GeneralizeVar by auto with wf typeclass_instances.
-    eapply @Interp_EvalWithBound; eauto with wf typeclass_instances.
+    rewrite <- Extract_GeneralizeVar; auto with wf typeclass_instances.
+    { eapply @Interp_EvalWithBound; eauto with wf typeclass_instances. }
+    { cbv [Proper] in *.
+      eapply type.and_for_each_lhs_of_arrow_Proper_impl_hetero1;
+        [ | eapply type.andb_bool_impl_and_for_each_lhs_of_arrow; [ | eassumption ] ];
+        [ | refine (fun t x y H => H) ];
+        cbv beta.
+      intros *; eapply ZRange.type.option.is_bounded_by_impl_eqv_refl. }
   Qed.
 
   Lemma Interp_PartialEvaluateWithListInfoFromBounds
         {opts : AbstractInterpretation.Options}
         {t} (E : Expr t)
         (Hwf : Wf E)
-        (Ht : type.is_not_higher_order t = true)
         (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)
@@ -1526,10 +1570,10 @@ Module Compilers.
                                    -> is_tighter_than_bool z r' = true)
           {t} (E : Expr t)
           (Hwf : Wf E)
-          (Ht : type.is_not_higher_order t = true)
           (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
           (b_out : ZRange.type.base.option.interp (type.final_codomain t))
           rv (Hrv : CheckedPartialEvaluateWithBounds relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations E b_in b_out = inl rv)
+          {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}
     : (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),
@@ -1543,17 +1587,49 @@ Module Compilers.
       [ 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 ]);
+        (*assert (b_in_Proper : Proper (type.and_for_each_lhs_of_arrow (@type.related _ _ (fun _ => eq))) b_in)
+          by (cbv [Proper] in *;
+              eapply type.and_for_each_lhs_of_arrow_Proper_impl_hetero1;
+              [ | eapply type.andb_bool_impl_and_for_each_lhs_of_arrow; [ | eassumption ] ];
+              [ | refine (fun t x y H => H) ];
+              cbv beta;
+              intros *; eapply ZRange.type.option.is_bounded_by_impl_eqv_refl);*)
         split;
-          repeat first [ rewrite !@GeneralizeVar.Interp_gen1_FromFlat_ToFlat by eauto with wf typeclass_instances
-                       | rewrite <- Extract_FromFlat_ToFlat by auto with typeclass_instances; apply Interp_PartialEvaluateWithBounds_bounded; auto
-                       | rewrite Extract_FromFlat_ToFlat by auto with wf typeclass_instances
-                       | progress intros
-                       | eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ]
-                       | solve [ eauto with wf typeclass_instances ]
-                       | erewrite !Interp_PartialEvaluateWithBounds
-                       | apply type.app_curried_Proper
-                       | apply expr.Wf_Interp_Proper_gen
-                       | progress intros ]
-        | eauto with wf typeclass_instances ].
+        repeat first [ rewrite !@GeneralizeVar.Interp_gen1_FromFlat_ToFlat by eauto with wf typeclass_instances
+                     | rewrite <- Extract_FromFlat_ToFlat by eauto with typeclass_instances; apply Interp_PartialEvaluateWithBounds_bounded; auto
+                     | rewrite Extract_FromFlat_ToFlat by eauto with wf typeclass_instances
+                     | progress intros
+                     | eapply ZRange.type.base.option.is_tighter_than_is_bounded_by; [ eassumption | ]
+                     | solve [ eauto with wf typeclass_instances ]
+                     | erewrite !Interp_PartialEvaluateWithBounds
+                     | apply type.app_curried_Proper
+                     | apply expr.Wf_Interp_Proper_gen
+                     | progress intros ]
+      | eauto with wf typeclass_instances ].
+  Qed.
+
+  Theorem CheckedPartialEvaluateWithBounds_Correct_first_order
+          {opts : AbstractInterpretation.Options}
+          (relax_zrange : zrange -> option zrange)
+          (assume_cast_truncates : bool)
+          (skip_annotations_under : forall t, ident t -> bool)
+          (strip_preexisting_annotations : bool)
+          (Hrelax : forall r r' z, is_tighter_than_bool z r = true
+                                   -> relax_zrange r = Some r'
+                                   -> is_tighter_than_bool z r' = true)
+          {t} (E : Expr t)
+          (Hwf : Wf E)
+          (Ht : type.is_not_higher_order t = true)
+          (b_in : type.for_each_lhs_of_arrow ZRange.type.option.interp t)
+          (b_out : ZRange.type.base.option.interp (type.final_codomain t))
+          rv (Hrv : CheckedPartialEvaluateWithBounds relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations E b_in b_out = inl rv)
+    : (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),
+          ZRange.type.base.option.is_bounded_by b_out (type.app_curried (Interp rv) arg1) = true
+          /\ type.app_curried (Interp rv) arg1 = type.app_curried (Interp E) arg2)
+      /\ Wf rv.
+  Proof.
+    eapply CheckedPartialEvaluateWithBounds_Correct; eauto with core typeclass_instances.
   Qed.
 End Compilers.
diff --git a/src/AbstractInterpretation/Wf.v b/src/AbstractInterpretation/Wf.v
index fb1c30b3b4..21ac4df51d 100644
--- a/src/AbstractInterpretation/Wf.v
+++ b/src/AbstractInterpretation/Wf.v
@@ -15,11 +15,13 @@ Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.Bool.Reflect.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
 Require Import Crypto.Util.Tactics.BreakMatch.
+Require Import Crypto.Util.Tactics.DoWithHyp.
 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.Util.HProp.
 Require Import Rewriter.Language.Language.
 Require Import Rewriter.Language.Inversion.
 Require Import Crypto.Language.InversionExtra.
@@ -58,25 +60,33 @@ Module Compilers.
               (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 value var := (@value base_type ident var abstract_domain').
+              {bottom'_Proper : forall t, Proper (abstract_domain'_R t) (bottom' t)}
+              (base_type_beq : base_type -> base_type -> bool)
+              {reflect_base_type_beq : reflect_rel eq base_type_beq}
+              {try_make_transport_base_type_cps : @type.try_make_transport_cpsT base_type}
+              {try_make_transport_base_type_cps_correct : type.try_make_transport_cps_correctT base_type}.
+
+      Local Notation value' var := (@value' base_type ident var abstract_domain').
       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')).
 
+      Context {default_expr : @DefaultValue.type.base.DefaultT _ (@expr abstract_domain)}. (* needed for impossible cases *)
+
+      (*Context {base_type_eq_Decidable : DecidableRel (@eq base_type)}.*)
+
       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 var1).
-        Local Notation value2 := (@value var2).
-        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' bottom').
-        Local Notation state_of_value2 := (@state_of_value base_type ident var2 abstract_domain' bottom').
+        Local Notation value'1 := (@value' var1).
+        Local Notation value'2 := (@value' var2).
+        Local Notation value1 := (@value base_type ident var1 abstract_domain').
+        Local Notation value2 := (@value 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
@@ -84,57 +94,58 @@ Module Compilers.
                      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 : bool -> forall t, ident t -> value_with_lets1 t)
-                (interp_ident2 : bool -> forall t, ident t -> value_with_lets2 t)
+                (interp_ident'1 : bool -> forall t, ident t -> UnderLets1 (value'1 t))
+                (interp_ident'2 : bool -> forall t, ident t -> UnderLets2 (value'2 t))
                 (skip_annotations_under : forall t, ident t -> bool).
         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 bottomify1 := (@bottomify base_type ident var1 abstract_domain' bottom').
-        Local Notation bottomify2 := (@bottomify base_type ident var2 abstract_domain' bottom').
-        Local Notation interp1 := (@interp base_type ident var1 abstract_domain' annotate1 bottom' skip_annotations_under interp_ident1).
-        Local Notation interp2 := (@interp base_type ident var2 abstract_domain' annotate2 bottom' skip_annotations_under interp_ident2).
-        Local Notation eval_with_bound'1 := (@eval_with_bound' base_type ident var1 abstract_domain' annotate1 bottom' skip_annotations_under interp_ident1).
-        Local Notation eval_with_bound'2 := (@eval_with_bound' base_type ident var2 abstract_domain' annotate2 bottom' skip_annotations_under interp_ident2).
-        Local Notation eval'1 := (@eval' base_type ident var1 abstract_domain' annotate1 bottom' skip_annotations_under interp_ident1).
-        Local Notation eval'2 := (@eval' base_type ident var2 abstract_domain' annotate2 bottom' skip_annotations_under interp_ident2).
+        Local Notation interp1 := (@interp base_type ident var1 try_make_transport_base_type_cps abstract_domain' annotate1 bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'1).
+        Local Notation interp2 := (@interp base_type ident var2 try_make_transport_base_type_cps abstract_domain' annotate2 bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'2).
+        Local Notation eval_with_bound'1 := (@eval_with_bound' base_type ident var1 try_make_transport_base_type_cps abstract_domain' annotate1 bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'1).
+        Local Notation eval_with_bound'2 := (@eval_with_bound' base_type ident var2 try_make_transport_base_type_cps abstract_domain' annotate2 bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'2).
+        Local Notation eval'1 := (@eval' base_type ident var1 try_make_transport_base_type_cps abstract_domain' annotate1 bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'1).
+        Local Notation eval'2 := (@eval' base_type ident var2 try_make_transport_base_type_cps abstract_domain' annotate2 bottom' skip_annotations_under default_expr abstract_interp_ident interp_ident'2).
         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').
+        Local Notation invert_default := (@invert_default base_type ident try_make_transport_base_type_cps abstract_domain' default_expr).
+        Local Notation invert_default' := (@invert_default' base_type ident try_make_transport_base_type_cps abstract_domain' default_expr).
 
         Definition abstract_domain_R {t} : relation (abstract_domain t)
           := type.related abstract_domain'_R.
 
+        Context {abstract_interp_ident_Proper : forall t, Proper (eq ==> @abstract_domain_R t) (abstract_interp_ident t)}.
+
         (** 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
+            [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)
+        Fixpoint wf_value' G {t} : value'1 t -> value'2 t -> Prop
+          := match t return value'1 t -> value'2 t -> Prop with
+             | type.base t => expr.wf G
              | type.arrow s d
                => fun v1 v2
                  => forall seg G' sv1 sv2,
                      G' = (seg ++ G)%list
-                     -> @wf_value seg s sv1 sv2
+                     -> abstract_domain_R (fst sv1) (fst sv2)
+                        /\ @wf_value' seg s (snd sv1) (snd sv2)
                      -> UnderLets.wf
-                         (fun G' => @wf_value G' d) G'
+                         (fun G' => @wf_value' G' d) G'
                          (v1 sv1) (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.
+        Definition wf_value G {t} : value1 t -> value2 t -> Prop
+          := fun v1 v2 => abstract_domain_R (fst v1) (fst v2)
+                          /\ UnderLets.wf (fun G' => wf_value' G') G (snd v1) (snd v2).
 
         Context (interp_ident_Proper
                  : forall G t idc1 idc2 (Hidc : idc1 = idc2) annotate_with_state,
-                    wf_value_with_lets G (interp_ident1 annotate_with_state t idc1) (interp_ident2 annotate_with_state t idc2)).
+                    UnderLets.wf (fun G' => wf_value' G') G (interp_ident'1 annotate_with_state t idc1) (interp_ident'2 annotate_with_state t idc2)).
 
         Global Instance bottom_Proper {t} : Proper abstract_domain_R (@bottom t) | 10.
         Proof using bottom'_Proper.
@@ -152,20 +163,17 @@ Module Compilers.
 
         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 bottom'_Proper.
-          clear -Hv type_base bottom'_Proper.
-          destruct t; [ destruct v1, v2, Hv | ]; cbn in *; cbv [respectful]; eauto; intros; apply bottom_Proper.
-        Qed.
+        Proof using Type. apply Hv. Qed.
 
         Local Hint Resolve (fun A (P : list A -> Prop) => ex_intro P nil) (fun A (x : A) (P : list A -> Prop) => ex_intro P (cons x nil)) : core.
         Local Hint Constructors expr.wf ex : core.
         Local Hint Unfold List.In : core.
 
-        Lemma wf_value_Proper_list G1 G2
+        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.
+              (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;
@@ -182,6 +190,49 @@ Module Compilers.
                          | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ] ].
         Qed.
 
+        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.
+          split; try apply Hwf.
+          eapply UnderLets.wf_Proper_list, Hwf; eauto using wf_value'_Proper_list.
+        Qed.
+
+        Local Ltac wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d
+          := first [ progress cbn [fst snd] in *
+                   | progress fold (@wf_value') in *
+                   | match goal with
+                     | [ |- wf_value _ (reflect1 _ _ _) (reflect2 _ _ _) ] => apply wf_reflect_s || apply wf_reflect_d
+                     | [ |- UnderLets.wf _ _ (UnderLets.splice (reify1 _ _ _ _) _) (UnderLets.splice (reify2 _ _ _ _) _) ]
+                       => eapply UnderLets.wf_splice; [ apply wf_reify_s || apply wf_reify_d | ]
+                     | [ |- UnderLets.wf _ _ (reify1 _ _ _ _) (reify2 _ _ _ _) ]
+                       => apply wf_reify_s || apply wf_reify_d
+                     | [ |- abstract_domain_R (state_of_value1 ?v1 ?x1) (state_of_value2 ?v2 ?x2) ]
+                       => eapply (state_of_value_Proper _ v1 v2); [ | change (abstract_domain_R x1 x2) ]
+                     end
+                   | progress cbn [wf_value'] in *
+                   | progress intros
+                   | progress subst
+                   | progress destruct_head'_and
+                   | progress destruct_head'_ex
+                   | progress cbv [respectful wf_value] in *
+                   | match goal with
+                     | [ |- ?x ++ ?y::?z ++ ?w = ?seg ++ ?z ++ ?w ] => unify seg (x ++ y::nil); cbn [List.app]; rewrite <- !app_assoc
+                     end
+                   | solve [ eauto | wf_t ]
+                   | apply annotate_Proper
+                   | apply UnderLets.wf_to_expr
+                   | break_innermost_match_step
+                   | eapply wf_value'_Proper_list; [ | eassumption ]
+                   | match goal with
+                     | [ |- UnderLets.wf _ _ _ _ ] => constructor
+                     | [ |- expr.wf _ _ _ ] => constructor
+                     | [ |- _ /\ _ ] => split
+                     | [ |- abstract_domain_R (state_of_value1 _) (state_of_value2 _) ]
+                       => eapply state_of_value_Proper
+                     end ].
         Fixpoint wf_reify (annotate_with_state : bool) (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),
@@ -204,53 +255,49 @@ Module Compilers.
           all: cbn [reify reflect] in *.
           all: fold (@reify2) (@reflect2) (@reify1) (@reflect1).
           all: cbn in *.
-          all: repeat first [ progress cbn [fst snd] in *
-                            | progress cbv [respectful] in *
-                            | progress intros
-                            | progress subst
-                            | progress destruct_head'_and
-                            | progress destruct_head'_ex
-                            | solve [ eauto | wf_t ]
-                            | apply annotate_Proper
-                            | apply UnderLets.wf_to_expr
-                            | break_innermost_match_step
-                            | match goal with
-                              | [ |- UnderLets.wf _ _ _ _ ] => constructor
-                              | [ |- expr.wf _ _ _ ] => constructor
-                              | [ He : forall seg G' sv1 sv2, G' = (seg ++ ?G)%list -> _ |- UnderLets.wf _ (?v :: ?G) (UnderLets.splice _ _) (UnderLets.splice _ _) ]
-                                => eapply UnderLets.wf_splice; [ apply (He (cons v nil)) | ]
-                              | [ |- UnderLets.wf _ _ (UnderLets.splice (reify1 _ _ _ _) _) (UnderLets.splice (reify2 _ _ _ _) _) ]
-                                => eapply UnderLets.wf_splice; [ apply wf_reify_s || apply wf_reify_d | ]
-                              | [ |- wf_value _ (reflect1 _ _ _) (reflect2 _ _ _) ] => apply wf_reflect_s || apply wf_reflect_d
-                              | [ H : wf_value _ ?x ?y |- wf_value _ ?x ?y ]
-                                => eapply wf_value_Proper_list; [ | eassumption ]
-                              | [ H : forall x y, ?R x y -> ?R' (?f x) (?g y) |- ?R' (?f _) (?g _) ]
-                                => apply H
-                              | [ |- ?R (state_of_value1 _) (state_of_value2 _) ] => eapply state_of_value_Proper
-                              end ].
+          all: repeat wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d.
+          all: try (eapply UnderLets.wf_splice; [ eassumption + apply wf_reify_s + apply wf_reify_d + apply wf_reflect_s + apply wf_reflect_d | ]).
+          all: repeat wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d.
+          all: try (eapply UnderLets.wf_splice; [ eassumption + apply wf_reify_s + apply wf_reify_d + apply wf_reflect_s + apply wf_reflect_d | ]).
+          all: repeat wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d.
+          all: try (eapply UnderLets.wf_splice; [ eassumption + apply wf_reify_s + apply wf_reify_d + apply wf_reflect_s + apply wf_reflect_d | ]).
+          all: repeat wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d.
+          all: try (apply wf_reify_s + apply wf_reify_d + apply wf_reflect_s + apply wf_reflect_d).
+          all: repeat wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d.
+          all: [ > ].
+          eapply UnderLets.wf_splice.
+          1: match goal with
+             | [ H : wf_value' ?G ?x ?y |- UnderLets.wf ?P ?G (?f (_, ?x)) (?g (_, ?y)) ]
+               => eapply UnderLets.wf_Proper_list_impl with (P1:=P) (P2:=P); revgoals
+             end;
+          [ exactly_once multimatch goal with H : _ |- _ => eapply H end | .. ].
+          all: repeat wf_reify_reflect_step wf_reflect_s wf_reflect_d wf_reify_s wf_reify_d.
+          all: instantiate (1:=_::nil); left; reflexivity.
         Qed.
 
-        Lemma wf_bottomify {t} G v1 v2
-              (Hwf : @wf_value G t v1 v2)
-          : wf_value_with_lets G (bottomify1 v1) (bottomify2 v2).
-        Proof using bottom'_Proper.
-          cbv [wf_value_with_lets] in *.
-          revert dependent G; induction t as [|s IHs d IHd]; intros;
-            cbn [bottomify wf_value]; fold (@value1) (@value2) in *; break_innermost_match;
-              constructor.
-          all: repeat first [ progress cbn [fst snd wf_value] in *
-                            | progress destruct_head'_and
-                            | assumption
-                            | apply bottom'_Proper
-                            | apply conj
-                            | progress intros
-                            | progress subst
-                            | solve [ eapply UnderLets.wf_splice; eauto ] ].
+        #[local] Existing Instance type.reflect_type_beq.
+
+        Lemma invert_default_Some {A B o t v}
+          : o = Some (existT _ t v) -> @invert_default A B t o = v.
+        Proof using try_make_transport_base_type_cps_correct.
+          intro; subst; cbv [invert_default Option.sequence_return projT1 projT2].
+          rewrite_type_transport_correct.
+          break_innermost_match; try now exfalso; reflect_hyps; congruence.
+          rewrite Reflect.eq_reflect_to_dec_true_refl; reflexivity.
+        Qed.
+
+        Lemma invert_default'_Some {A B C o t v}
+          : o = Some (existT _ t v) -> @invert_default' A B C t o = v.
+        Proof using try_make_transport_base_type_cps_correct.
+          intro; subst; cbv [invert_default' Option.sequence_return projT1 projT2].
+          rewrite_type_transport_correct.
+          break_innermost_match; try now exfalso; reflect_hyps; congruence.
+          rewrite Reflect.eq_reflect_to_dec_true_refl; reflexivity.
         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 *
+          repeat first [ progress cbv [wf_value abstract_domain_R respectful Base_value' project_value' Option.sequence_return] 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
@@ -258,17 +305,21 @@ Module Compilers.
                        | progress destruct_head'_ex
                        | progress destruct_head'_or
                        | eapply UnderLets.wf_splice
+                       | erewrite invert_default_Some by reflexivity
+                       | erewrite invert_default'_Some by reflexivity
                        | match goal with
-                         | [ |- UnderLets.wf _ _ (bottomify1 _) (bottomify2 _) ] => apply wf_bottomify
                          | [ |- UnderLets.wf _ _ _ _ ] => constructor
                          | [ |- and _ _ ] => apply conj
+                         | [ H : _ = snd ?x |- _ ] => is_var x; destruct x
+                         | [ H : _ = fst ?x |- _ ] => is_var x; destruct x
                          end
-                       | eapply wf_value_Proper_list; [ | solve [ eauto ] ]
-                       | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto ] ]
+                       | eapply wf_value'_Proper_list; [ | solve [ eauto | split_and; eauto ] ]
+                       | eapply UnderLets.wf_Proper_list; [ | | solve [ eauto | split_and; eauto ] ]
                        | match goal with
                          | [ H : _ |- _ ] => eapply H; clear H; solve [ wf_interp_t ]
                          end
-                       | break_innermost_match_step ].
+                       | break_innermost_match_step
+                       | progress eliminate_hprop_eq ].
 
         Local Notation skip_annotations_for_App := (@skip_annotations_for_App base_type ident skip_annotations_under).
 
@@ -299,12 +350,39 @@ Module Compilers.
                            end ].
         Qed.
 
-        Lemma wf_interp (annotate_with_state : bool) 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 annotate_with_state e1) (interp2 annotate_with_state e2).
-        Proof using annotate_Proper bottom'_Proper interp_ident_Proper.
-          revert dependent G'; revert annotate_with_state; induction Hwf; intros; cbn [interp];
+        Lemma wf_interp (annotate_with_state : bool) (G : list { t : _ & value1 t * value2 t * abstract_domain t * abstract_domain t }%type) G12 G34 G' {t} (e1 : @expr (@value1) t) (est1 : @expr abstract_domain t) (e2 : @expr (@value2) t) (est2 : @expr abstract_domain t)
+          (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12)
+          (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34)
+          (Hwf : expr.wf4 G e1 e2 est1 est2)
+          (Hwf' : expr.wf G34 est1 est2)
+          (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2)
+          (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2)
+          : wf_value G' (interp1 annotate_with_state e1 est1) (interp2 annotate_with_state e2 est2).
+        Proof using abstract_interp_ident_Proper annotate_Proper bottom'_Proper interp_ident_Proper try_make_transport_base_type_cps_correct.
+          revert dependent G12; revert dependent G34; revert dependent G'; revert annotate_with_state; induction Hwf; intros; cbn [interp];
+            repeat match goal with
+              | [ H : List.In (existT _ ?t (?v1, ?v2, ?v3, ?v4)) ?G, H' : List.map _ ?G = ?G12 |- _ ]
+                => unique assert (List.In (existT _ t (v1, v2)) G12)
+                  by (rewrite <- H'; revert H; rewrite in_map_iff; eexists; split; try eassumption; reflexivity)
+              | [ H : List.In (existT _ ?t (?v1, ?v2, ?v3, ?v4)) ?G, H' : List.map _ ?G = ?G34 |- _ ]
+                => unique assert (List.In (existT _ t (v3, v4)) G34)
+                  by (rewrite <- H'; revert H; rewrite in_map_iff; eexists; split; try eassumption; reflexivity)
+              | [ HG : List.map ?f ?G = ?G12, H : forall v1 v2 v3 v4, expr.wf4 (@?v v1 v2 v3 v4 :: ?G) (@?e1 v1 v2) (@?e2 v1 v2) _ _ |- _ ]
+                => let v' := (eval cbn in (fun v1 v2 => f (v v1 v2 bottom bottom))) in
+                   let lem := (eval cbv beta in (forall v1 v2, expr.wf (v' v1 v2 :: G12) (e1 v1 v2) (e2 v1 v2))) in
+                   unique assert lem
+                     by (intros v1 v2; specialize (H v1 v2 bottom bottom);
+                         apply expr.wf_of_wf4_default in H; subst G12; cbn [List.map] in H;
+                         apply H; split; apply bottom)
+              | [ HG : List.map ?f ?G = ?G12, H : expr.wf4 ?G ?e1 ?e2 _ _ |- _ ]
+                => unique assert (expr.wf G12 e1 e2)
+                  by (apply expr.wf_of_wf4_default in H; subst G12; cbn [List.map] in H;
+                      apply H; split; apply bottom)
+              | [ HG : List.map ?f ?G = ?G34, H : expr.wf4 ?G _ _ ?e3 ?e4 |- _ ]
+                => unique assert (expr.wf G34 e3 e4)
+                  by (apply expr.wf_of_wf4_default in H; subst G34; cbn [List.map] in H;
+                      apply H; split; apply bottom)
+              end;
             try solve [ apply interp_ident_Proper; auto
                       | eauto ];
             match goal with
@@ -312,27 +390,97 @@ Module Compilers.
               => match goal with
                  | [ |- context[skip_annotations_for_App ?e2v] ]
                    => epose proof (wf_skip_annotations_for_App (e1:=e1v) (e2:=e2v) (G:=G') ltac:(solve [ wf_t ]));
-                        generalize dependent (skip_annotations_for_App e1v);
-                        generalize dependent (skip_annotations_for_App e2v); intros;
-                          subst
+                      generalize dependent (skip_annotations_for_App e1v);
+                      generalize dependent (skip_annotations_for_App e2v); intros;
+                      subst
                  end
             end;
             wf_interp_t.
+          all: lazymatch goal with
+               | [ H : type.related ?R ?x ?y |- type.related ?R (expr.interp ?ii1 ?f1 ?x) (expr.interp ?ii2 ?f2 ?y) ]
+                 => is_var x; is_var y;
+                    revert x y H;
+                    change (type.related R (expr.interp ii1 f1) (expr.interp ii2 f2));
+                    eapply expr.wf_interp_Proper_gen2; eauto
+               | _ => idtac
+               end.
+          all: repeat match goal with
+                 | [ H : invert_Abs (expr.Abs _) = _ |- _ ]
+                   => cbv in H; inversion_option; subst
+                 end.
+          all: expr.inversion_wf_constr; wf_interp_t.
+          all: try now
+                 (
+                   do_with_exactly_one_hyp ltac:(fun H => eapply H; clear H);
+                   lazymatch goal with
+                   | [ |- expr.wf _ _ _ ] => now eauto
+                   | _ => idtac
+                   end;
+                   try reflexivity;
+                   [ > wf_interp_t .. ];
+                   cbn [List.In List.map] in *;
+                   wf_interp_t
+                 ).
+          all: try now
+                 (
+                   eapply UnderLets.wf_Proper_list_impl;
+                   [ .. | do_with_exactly_one_hyp ltac:(fun H => eapply H; clear H) ];
+                   try reflexivity;
+                   [ .. | wf_interp_t ];
+                   wf_interp_t
+                 ).
+          all: try now
+                 (
+                   eapply expr.wf_interp_Proper_gen2;
+                   lazymatch goal with
+                   | [ |- expr.wf _ _ _ ] => now eauto
+                   | _ => idtac
+                   end;
+                   cbn [List.map List.In];
+                   wf_interp_t
+                 ).
+          all: try now
+                 (
+                   do_with_hyp' ltac:(fun H => eapply H; clear H);
+                   try reflexivity;
+                   cbn [List.In List.map] in *;
+                   wf_interp_t
+                 ).
+          all: try do_with_hyp'
+                 ltac:(fun H
+                       => now
+                            (
+                              eapply H;
+                              try reflexivity;
+                              wf_interp_t;
+                              cbn [List.In List.map] in *;
+                              wf_interp_t
+                            )
+                      ).
+          Unshelve.
+          all: assumption.
         Qed.
 
-        Lemma wf_eval_with_bound' (annotate_with_state : bool) 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 annotate_with_state t e1 st1) (@eval_with_bound'2 annotate_with_state 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. }
+        Lemma wf_eval_with_bound' (annotate_with_state : bool) G G12 G34 G' {t} e1 e2 est1 est2 (He : expr.wf4 G e1 e2 est1 est2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
+          (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12)
+          (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34)
+          (Hwf' : expr.wf G34 est1 est2)
+          (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2)
+          (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2)
+          : expr.wf G' (@eval_with_bound'1 annotate_with_state t e1 est1 st1) (@eval_with_bound'2 annotate_with_state t e2 est2 st2).
+        Proof using abstract_interp_ident_Proper annotate_Proper bottom'_Proper interp_ident_Proper try_make_transport_base_type_cps_correct.
+          eapply UnderLets.wf_to_expr, wf_reify; eauto; [].
+          eapply wf_interp; try eassumption.
         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.
+        Lemma wf_eval' G G12 G34 G' {t} e1 e2 est1 est2 (He : expr.wf4 G e1 e2 est1 est2)
+          (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12)
+          (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34)
+          (Hwf' : expr.wf G34 est1 est2)
+          (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2)
+          (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2)
+          : expr.wf G' (@eval'1 t e1 est1) (@eval'2 t e2 est2).
+        Proof using abstract_interp_ident_Proper annotate_Proper bottom'_Proper interp_ident_Proper try_make_transport_base_type_cps_correct.
           eapply wf_eval_with_bound'; eauto; apply bottom_for_each_lhs_of_arrow_Proper.
         Qed.
 
@@ -389,14 +537,14 @@ Module Compilers.
 
         Section with_var2.
           Context {var1 var2 : type -> Type}.
-          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).
+          Local Notation wf_value' := (@wf_value' base.type ident abstract_domain' abstract_domain'_R var1 var2).
           Context (annotate_expr1 : forall t, abstract_domain' t -> option (@expr var1 (t -> t)))
                   (annotate_expr2 : forall t, abstract_domain' t -> option (@expr var2 (t -> t)))
                   (is_annotated_for1 : forall t t', @expr var1 t -> abstract_domain' t' -> bool)
                   (is_annotated_for2 : forall t t', @expr var2 t -> abstract_domain' t' -> bool)
-                  (strip_annotation1 : forall t, ident t -> option (value _ t))
-                  (strip_annotation2 : forall t, ident t -> option (value _ t))
+                  (strip_annotation1 : forall t, ident t -> option (value' _ t))
+                  (strip_annotation2 : forall t, ident t -> option (value' _ t))
                   (annotation_to_cast1 : forall s d, @expr var1 (s -> d) -> option (@expr var1 s -> @expr var1 d))
                   (annotation_to_cast2 : forall s d, @expr var2 (s -> d) -> option (@expr var2 s -> @expr var2 d))
                   (skip_annotations_under : forall t, ident t -> bool)
@@ -416,7 +564,7 @@ Module Compilers.
                            (@is_annotated_for2 t t' e2)}
                   {wf_strip_annotation
                    : forall G t idc,
-                      option_eq (wf_value G)
+                      option_eq (wf_value' G)
                                 (@strip_annotation1 t idc)
                                 (@strip_annotation2 t idc)}.
 
@@ -428,8 +576,8 @@ Module Compilers.
           Local Notation annotate_base2 := (@ident.annotate_base var2 abstract_domain' annotate_expr2 is_annotated_for2).
           Local Notation annotate_with_expr1 := (@ident.annotate_with_expr var1 abstract_domain' annotate_expr1 is_annotated_for1).
           Local Notation annotate_with_expr2 := (@ident.annotate_with_expr var2 abstract_domain' annotate_expr2 is_annotated_for2).
-          Local Notation interp_ident1 := (@ident.interp_ident var1 abstract_domain' annotate_expr1 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for1 strip_annotation1).
-          Local Notation interp_ident2 := (@ident.interp_ident var2 abstract_domain' annotate_expr2 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for2 strip_annotation2).
+          Local Notation interp_ident'1 := (@ident.interp_ident' var1 abstract_domain' annotate_expr1 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for1 strip_annotation1).
+          Local Notation interp_ident'2 := (@ident.interp_ident' var2 abstract_domain' annotate_expr2 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for2 strip_annotation2).
           Local Notation reflect1 := (@reflect base.type ident var1 abstract_domain' annotate1 bottom').
           Local Notation reflect2 := (@reflect base.type ident var2 abstract_domain' annotate2 bottom').
 
@@ -608,23 +756,30 @@ Module Compilers.
                               | progress cbn [type.decode f_equal eq_rect fst snd] in *
                               | solve [ wf_t ] ] ].
           Qed.
-          Local Ltac type_of_value v :=
+          Local Ltac type_of_value' v :=
             lazymatch v with
             | (abstract_domain ?t * _)%type => t
+            | expr ?t => t
             | (?a -> UnderLets _ ?b)
-              => let a' := type_of_value a in
-                let b' := type_of_value b in
+              => let a' := type_of_value' a in
+                let b' := type_of_value' b in
                 constr:(type.arrow a' b')
+            | ?v => fail 0 "type_of_value': unrecognized:" v
             end.
           Local Opaque ident.ident_Literal.
           Lemma wf_interp_ident_nth_default (annotate_with_state : bool) G T
-            : wf_value_with_lets G (@interp_ident1 annotate_with_state _ (@ident.List_nth_default T)) (@interp_ident2 annotate_with_state _ (@ident.List_nth_default T)).
+            : UnderLets.wf (fun G' => wf_value' G') G (@interp_ident'1 annotate_with_state _ (@ident.List_nth_default T)) (@interp_ident'2 annotate_with_state _ (@ident.List_nth_default T)).
           Proof using abstract_interp_ident_Proper annotate_expr_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper.
-            cbv [wf_value_with_lets wf_value ident.interp_ident]; constructor; cbn -[abstract_domain_R abstract_domain].
-            { intros; subst.
-              destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *.
+            cbv [wf_value wf_value' ident.interp_ident']; constructor; cbn -[abstract_domain_R abstract_domain].
+            all: intros; subst.
+            all: destruct_head'_prod; destruct_head'_and; cbn [fst snd] in *.
+            all:
               repeat first [ progress subst
                            | lazymatch goal with
+                             | [ H : wf_value' _ (reify_list _) _ |- _ ]
+                               => progress cbn [wf_value'] in H
+                             | [ H : wf_value' _ _ (reify_list _) |- _ ]
+                               => progress cbn [wf_value'] in H
                              | [ 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 |- _ ]
@@ -655,8 +810,8 @@ Module Compilers.
                                    | [ |- expr _ -> _ -> _ ]
                                      => refine (expr.wf G)
                                    | [ |- ?T -> _ -> _ ]
-                                     => let t := type_of_value T in
-                                       refine (@wf_value G t)
+                                     => let t := type_of_value' T in
+                                       refine (@wf_value' G t)
                                    end
                                  | | ]
                              | [ |- UnderLets.wf ?Q ?G (UnderLets.Base _) (UnderLets.Base _) ]
@@ -666,8 +821,8 @@ Module Compilers.
                              | [ 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)
+                               => unique pose proof (@nth_error_value_length _ _ _ _ H);
+                                  unique pose proof (@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
@@ -686,7 +841,7 @@ Module Compilers.
                              end
                            | progress inversion_option
                            | progress intros
-                           | progress cbn [fst snd value] in *
+                           | progress cbn [fst snd value'] in *
                            | progress destruct_head'_prod
                            | progress destruct_head'_ex
                            | progress destruct_head'_and
@@ -698,10 +853,9 @@ Module Compilers.
                            | progress expr.inversion_expr
                            | handle_Forall2_step
                            | 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 (abstract_interp_ident_Proper _ (@ident.List_nth_default _) _ eq_refl); assumption
                                    | eapply wf_update_annotation; wf_t
                                    | wf_t
                                    | match goal with
@@ -723,14 +877,14 @@ Module Compilers.
                            | progress expr.inversion_wf_one_constr
                            | progress expr.invert_match
                            | match goal with
-                             | [ |- wf_value _ _ _ ] => progress hnf
-                             end ]. }
+                             | [ |- wf_value' _ _ _ ] => progress hnf
+                             end ].
           Qed.
 
           Lemma wf_interp_ident_not_nth_default_nostrip (annotate_with_state : bool) G {t} (idc : ident t)
-            : wf_value_with_lets G (Base (reflect1 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc))) (Base (reflect2 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc))).
+            : wf_value G (reflect1 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc)) (reflect2 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc)).
           Proof using abstract_interp_ident_Proper annotate_expr_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper.
-            constructor; eapply wf_reflect;
+            constructor; unshelve eapply wf_reflect;
               solve [ apply bottom'_Proper
                     | apply wf_annotate
                     | repeat constructor
@@ -738,30 +892,31 @@ Module Compilers.
           Qed.
 
           Lemma wf_interp_ident_not_nth_default (annotate_with_state : bool) G {t} (idc : ident t)
-            : (wf_value_with_lets G)
-                (Base match strip_annotation1 _ idc with
-                      | Some v => v
-                      | None => reflect1 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc)
-                      end)
-                (Base match strip_annotation2 _ idc with
-                      | Some v => v
-                      | None => reflect2 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc)
-                      end).
+            : (UnderLets.wf (fun G' => wf_value' G') G)
+                (match strip_annotation1 _ idc with
+                 | Some v => Base v
+                 | None => project_value' _ (reflect1 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc))
+                 end)
+                (match strip_annotation2 _ idc with
+                 | Some v => Base v
+                 | None => project_value' _ (reflect2 annotate_with_state (###idc)%expr (abstract_interp_ident _ idc))
+                 end).
           Proof using abstract_interp_ident_Proper annotate_expr_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper wf_strip_annotation.
             pose proof (wf_strip_annotation G _ idc).
             break_innermost_match; cbn [option_eq] in *;
               solve [ exfalso; assumption
                     | congruence
                     | apply wf_interp_ident_not_nth_default_nostrip
-                    | constructor; assumption ].
+                    | constructor; assumption
+                    | split; [ now apply abstract_interp_ident_Proper | constructor; assumption ] ].
           Qed.
 
           Lemma wf_interp_ident G {t} idc1 idc2 (Hidc : idc1 = idc2) (annotate_with_state : bool)
-            : wf_value_with_lets G (@interp_ident1 annotate_with_state t idc1) (@interp_ident2 annotate_with_state t idc2).
+            : UnderLets.wf (fun G' => wf_value' G') G (@interp_ident'1 annotate_with_state t idc1) (@interp_ident'2 annotate_with_state t idc2).
           Proof using abstract_interp_ident_Proper annotate_expr_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper wf_strip_annotation.
-            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 ].
+            subst idc2; destruct idc1;
+              first [ apply wf_interp_ident_not_nth_default
+                    | apply wf_interp_ident_nth_default ].
           Qed.
 
           Local Notation strip_all_annotations'1 := (@partial.ident.strip_all_annotations' var1 annotation_to_cast1 skip_annotations_under).
@@ -795,26 +950,38 @@ Module Compilers.
 
           Local Notation eval_with_bound1 := (@partial.ident.eval_with_bound var1 abstract_domain' annotate_expr1 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for1 strip_annotation1 skip_annotations_under).
           Local Notation eval_with_bound2 := (@partial.ident.eval_with_bound var2 abstract_domain' annotate_expr2 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for2 strip_annotation2 skip_annotations_under).
-          Lemma wf_eval_with_bound (annotate_with_state : bool) {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 annotate_with_state t e1 st1) (@eval_with_bound2 annotate_with_state t e2 st2).
+
+          Lemma wf_eval_with_bound (annotate_with_state : bool) {t} G G12 G34 G' e1 e2 est1 est2 (Hwf : expr.wf4 G e1 e2 est1 est2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
+            (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12)
+            (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34)
+            (Hwf' : expr.wf G34 est1 est2)
+            (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2)
+            (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2)
+            : expr.wf G' (@eval_with_bound1 annotate_with_state t e1 est1 st1) (@eval_with_bound2 annotate_with_state t e2 est2 st2).
           Proof using abstract_interp_ident_Proper annotate_expr_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper wf_strip_annotation.
             eapply wf_eval_with_bound';
               solve [ eassumption
                     | eapply wf_annotate
-                    | eapply wf_interp_ident ].
+                    | eapply wf_interp_ident
+                    | typeclasses eauto ].
           Qed.
 
           Local Notation eval1 := (@partial.ident.eval var1 abstract_domain' annotate_expr1 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for1 strip_annotation1).
           Local Notation eval2 := (@partial.ident.eval var2 abstract_domain' annotate_expr2 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for2 strip_annotation2).
-          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).
+
+          Lemma wf_eval {t} G G12 G34 G' e1 e2 est1 est2 (Hwf : expr.wf4 G e1 e2 est1 est2)
+            (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12)
+            (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34)
+            (Hwf' : expr.wf G34 est1 est2)
+            (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2)
+            (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2)
+            : expr.wf G' (@eval1 t e1 est1) (@eval2 t e2 est2).
           Proof using abstract_interp_ident_Proper annotate_expr_Proper bottom'_Proper extract_list_state_length extract_list_state_rel extract_option_state_rel is_annotated_for_Proper wf_strip_annotation.
             eapply wf_eval';
               solve [ eassumption
                     | eapply wf_annotate
-                    | eapply wf_interp_ident ].
+                    | eapply wf_interp_ident
+                    | typeclasses eauto ].
           Qed.
 
           Local Notation eta_expand_with_bound1 := (@partial.ident.eta_expand_with_bound var1 abstract_domain' annotate_expr1 bottom' abstract_interp_ident extract_list_state extract_option_state is_annotated_for1).
@@ -837,7 +1004,7 @@ Module Compilers.
       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)).
-      Local Notation wf_value := (@wf_value base.type ident abstract_domain' (fun t => abstract_domain'_R t)).
+      Local Notation wf_value' := (@wf_value' base.type ident abstract_domain' (fun t => abstract_domain'_R t)).
 
       Lemma annotate_expr_Proper {relax_zrange var1 var2} {t} s1 s2
         : abstract_domain'_R t s1 s2
@@ -877,12 +1044,12 @@ Module Compilers.
               (#(@ident.Literal base.type.zrange r1%zrange), #(@ident.Literal base.type.zrange r2%zrange))%expr_pat).
 
       Lemma wf_always_strip_annotation {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) {var1 var2} G {t} idc
-        : option_eq (wf_value G)
+        : option_eq (wf_value' G)
                     (always_strip_annotation assume_cast_truncates (var:=var1) t idc)
                     (always_strip_annotation assume_cast_truncates (var:=var2) t idc).
       Proof using Type.
         cbv [always_strip_annotation]; break_innermost_match; try reflexivity;
-          cbn [option_eq wf_value].
+          cbn [option_eq wf_value'].
         all: repeat first [ progress intros
                           | assumption
                           | progress subst
@@ -899,7 +1066,7 @@ Module Compilers.
       Qed.
 
       Lemma wf_strip_annotation {opts : AbstractInterpretation.Options} (assume_cast_truncates : bool) (strip_annotations : bool) {var1 var2} G {t} idc
-        : option_eq (wf_value G)
+        : option_eq (wf_value' G)
                     (strip_annotation assume_cast_truncates strip_annotations (var:=var1) t idc)
                     (strip_annotation assume_cast_truncates strip_annotations (var:=var2) t idc).
       Proof using Type.
@@ -1041,11 +1208,15 @@ Module Compilers.
 
       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 {opts : AbstractInterpretation.Options} {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' (t:=t) (eval (var:=var1) e1) (eval (var:=var2) e2).
+        Local Notation wf_value := (@wf_value base.type ident abstract_domain' (fun t => abstract_domain'_R t) var1 var2).
+
+        Lemma wf_eval {opts : AbstractInterpretation.Options} {t} G G12 G34 G' e1 e2 est1 est2 (Hwf : expr.wf4 G e1 e2 est1 est2)
+          (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12)
+          (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34)
+          (Hwf' : expr.wf G34 est1 est2)
+          (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2)
+          (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2)
+          : expr.wf G' (t:=t) (eval (var:=var1) e1 est1) (eval (var:=var2) e2 est2).
         Proof using Type.
           eapply ident.wf_eval;
             solve [ eassumption
@@ -1062,11 +1233,15 @@ Module Compilers.
           : expr.wf G (@strip_all_annotations strip_annotations_under var1 t e1) (@strip_all_annotations strip_annotations_under var2 t e2).
         Proof using Type. revert Hwf; apply ident.wf_strip_all_annotations, @wf_annotation_to_cast. Qed.
 
-        Lemma wf_eval_with_bound {opts : AbstractInterpretation.Options} {relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations 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)
+        Lemma wf_eval_with_bound {opts : AbstractInterpretation.Options} {relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations t} G G12 G34 G' e1 e2 est1 est2 (Hwf : expr.wf4 G e1 e2 est1 est2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
+          (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12)
+          (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34)
+          (Hwf' : expr.wf G34 est1 est2)
+          (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2)
+          (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2)
           : expr.wf G' (var1:=var1) (var2:=var2) (t:=t)
-                    (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e1 st1)
-                    (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e2 st2).
+                    (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e1 est1 st1)
+                    (eval_with_bound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e2 est2 st2).
         Proof using Type.
           eapply ident.wf_eval_with_bound;
             solve [ eassumption
@@ -1079,9 +1254,13 @@ Module Compilers.
                   | apply is_annotated_for_Proper ].
         Qed.
 
-        Lemma wf_strip_annotations {opts : AbstractInterpretation.Options} {assume_cast_truncates} {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' (t:=t) (strip_annotations assume_cast_truncates (var:=var1) e1 st1) (strip_annotations assume_cast_truncates (var:=var2) e2 st2).
+        Lemma wf_strip_annotations {opts : AbstractInterpretation.Options} {assume_cast_truncates} {t} G G12 G34 G' e1 e2 est1 est2 (Hwf : expr.wf4 G e1 e2 est1 est2) st1 st2 (Hst : type.and_for_each_lhs_of_arrow (@abstract_domain_R) st1 st2)
+          (HG12 : List.map (fun '(existT t (v1, v2, _, _)) => existT _ t (v1, v2)) G = G12)
+          (HG34 : List.map (fun '(existT t (_, _, v3, v4)) => existT _ t (v3, v4)) G = G34)
+          (Hwf' : expr.wf G34 est1 est2)
+          (HGG' : forall t v1 v2, List.In (existT _ t (v1, v2)) G12 -> wf_value G' v1 v2)
+          (HGG'' : forall t v1 v2, List.In (existT _ t (v1, v2)) G34 -> abstract_domain_R v1 v2)
+          : expr.wf G' (t:=t) (strip_annotations assume_cast_truncates (var:=var1) e1 est1 st1) (strip_annotations assume_cast_truncates (var:=var2) e2 est2 st2).
         Proof using Type.
           eapply ident.wf_eval_with_bound;
             solve [ eassumption
@@ -1115,19 +1294,19 @@ Module Compilers.
 
       Lemma Wf_Eval {opts : AbstractInterpretation.Options} {t} (e : Expr t) (Hwf : Wf e) : Wf (Eval e).
       Proof using Type.
-        intros ??; eapply wf_eval with (G:=nil); cbn [List.In]; try apply Hwf; tauto.
+        intros ??; cbv [Eval Let_In]; eapply wf_eval with (G:=nil); try reflexivity; cbn [List.In List.map]; try apply expr.Wf4_of_Wf; try apply GeneralizeVar.Wf_FromFlat_ToFlat, Hwf; tauto.
       Qed.
 
       Lemma Wf_EvalWithBound {opts : AbstractInterpretation.Options} {relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound)
         : Wf (EvalWithBound relax_zrange assume_cast_truncates skip_annotations_under strip_preexisting_annotations e bound).
       Proof using Type.
-        intros ??; eapply wf_eval_with_bound with (G:=nil); cbn [List.In]; try apply Hwf; tauto.
+        intros ??; cbv [EvalWithBound Let_In]; eapply wf_eval_with_bound with (G:=nil); try reflexivity; cbn [List.In List.map]; try apply expr.Wf4_of_Wf; try apply GeneralizeVar.Wf_FromFlat_ToFlat, Hwf; tauto.
       Qed.
 
       Lemma Wf_StripAnnotations {opts : AbstractInterpretation.Options} {assume_cast_truncates} {t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound)
         : Wf (StripAnnotations assume_cast_truncates e bound).
       Proof using Type.
-        intros ??; eapply wf_strip_annotations with (G:=nil); cbn [List.In]; try tauto; apply Hwf.
+        intros ??; cbv [StripAnnotations]; eapply wf_strip_annotations with (G:=nil); try reflexivity; cbn [List.In List.map]; try apply expr.Wf4_of_Wf; try apply Hwf; tauto.
       Qed.
 
       Lemma Wf_EtaExpandWithBound {relax_zrange t} (e : Expr t) bound (Hwf : Wf e) (bound_valid : Proper (type.and_for_each_lhs_of_arrow (@abstract_domain_R)) bound)
diff --git a/src/AbstractInterpretation/ZRangeProofs.v b/src/AbstractInterpretation/ZRangeProofs.v
index 0a6cca2ef6..f09333f70a 100644
--- a/src/AbstractInterpretation/ZRangeProofs.v
+++ b/src/AbstractInterpretation/ZRangeProofs.v
@@ -44,9 +44,12 @@ Require Import Crypto.Util.Tactics.PrintGoal.
 Require Import Crypto.Language.PreExtra.
 Require Import Crypto.CastLemmas.
 Require Import Crypto.AbstractInterpretation.ZRange.
+Require Import Crypto.AbstractInterpretation.ZRangeCommonProofs.
 
 Module Compilers.
   Import AbstractInterpretation.ZRange.Compilers.
+  Import AbstractInterpretation.ZRangeCommonProofs.Compilers.
+  Import Rewriter.Language.Wf.Compilers. (* for properties about type.related_hetero *)
   Export ZRange.Settings.
 
   Module ZRange.
@@ -65,11 +68,29 @@ Module Compilers.
           -> type.related_hetero (fun t x v => ZRange.type.base.option.is_bounded_by x v = true) x v.
         Proof. induction t; cbn in *; intuition congruence. Qed.
 
+        Lemma is_bounded_by_impl_related_hetero_and_Proper {skip_base} t
+              (x : ZRange.type.option.interp t) (v : type.interp base.interp t)
+        : ZRange.type.option.is_bounded_by x v = true
+          -> type.related_hetero_and_Proper (skip_base:=skip_base) (fun _ => eq) (fun _ => eq) (fun t x v => ZRange.type.base.option.is_bounded_by x v = true) x v.
+        Proof. induction t; cbn in *; break_innermost_match; intuition congruence. Qed.
+
         Lemma is_bounded_by_impl_eqv_refl t
+          (x : ZRange.type.option.interp t) (v : type.interp base.interp t)
+          : ZRange.type.option.is_bounded_by x v = true
+            -> x == x /\ v == v.
+        Proof. induction t; cbn; split; try reflexivity; try congruence. Qed.
+
+        Lemma is_bounded_by_impl_eqv_refl1 t
+          (x : ZRange.type.option.interp t) (v : type.interp base.interp t)
+          : ZRange.type.option.is_bounded_by x v = true
+            -> x == x.
+        Proof. intros; eapply is_bounded_by_impl_eqv_refl; eassumption. Qed.
+
+        Lemma is_bounded_by_impl_eqv_refl2 t
           (x : ZRange.type.option.interp t) (v : type.interp base.interp t)
           : ZRange.type.option.is_bounded_by x v = true
             -> v == v.
-        Proof. induction t; cbn; try reflexivity; try congruence. Qed.
+        Proof. intros; eapply is_bounded_by_impl_eqv_refl; eassumption. Qed.
 
         Lemma andb_bool_for_each_lhs_of_arrow_is_bounded_by_impl_and_for_each_lhs_of_arrow_eqv_refl t
           (x : type.for_each_lhs_of_arrow ZRange.type.option.interp t) (v : type.for_each_lhs_of_arrow (type.interp base.interp) t)
@@ -79,7 +100,7 @@ Module Compilers.
           induction t; cbn; [ reflexivity | ].
           rewrite Bool.andb_true_iff.
           intros [H0 H1].
-          split; eauto using is_bounded_by_impl_eqv_refl.
+          split; eauto using is_bounded_by_impl_eqv_refl2.
         Qed.
       End option.
     End type.
@@ -95,6 +116,14 @@ Module Compilers.
                   (fun t st v => ZRange.type.base.option.is_bounded_by st v = true)
                   (ZRange.ident.option.interp assume_cast_truncates idc)
                   (ident.interp idc)).
+          Local Notation interp_is_related_and_Proper idc
+            := (type.related_hetero_and_Proper
+                  (skip_base:=true)
+                  (fun t => eq)
+                  (fun t => eq)
+                  (fun t st v => ZRange.type.base.option.is_bounded_by st v = true)
+                  (ZRange.ident.option.interp assume_cast_truncates idc)
+                  (ident.interp idc)).
 
           Local Ltac z_cast_t :=
             cbn [type.related_hetero ZRange.ident.option.interp ident.interp respectful_hetero type.interp ZRange.type.base.option.interp ZRange.type.base.interp base.interp base.base_interp ZRange.type.base.option.Some];
@@ -603,9 +632,13 @@ Module Compilers.
                break_innermost_match; apply Bool.andb_true_iff; split; apply Z.leb_le; try apply Z.le_sub_1_iff; auto with zarith. }
           Qed.
 
-          Lemma interp_related {t} (idc : ident t) : interp_is_related idc.
+          (** In abstract interpretation, we only need this version of the lemma for less-than-third-order types, but in Assembly/Symbolic, we use it for all identifiers *)
+          Lemma interp_related {t} (idc : ident t) (*H : type.is_not_higher_order_than 3 t = true*) : interp_is_related idc.
           Proof using Type.
             destruct idc.
+            (*
+            (** clear out higher-than-third-order types *)
+            all: cbn in H; try congruence.*)
             all: lazymatch goal with
                  | [ |- context[ident.Z_cast] ] => apply interp_related_Z_cast
                  | [ |- context[ident.Z_cast2] ] => apply interp_related_Z_cast2
@@ -717,13 +750,24 @@ Module Compilers.
                                => Z.div_mod_to_quot_rem; nia
                              end
                            | intros; mul_by_halves_t ].
+            all: try solve [ non_arith_t; Z.ltb_to_lt; reflexivity ].
             (** For command-line debugging, we display goals that should not remain *)
-            all: [ > idtac "WARNING: Remaining goal:"; print_context_and_goal () .. | | ].
-            { intros.
-              rewrite Z.le_sub_1_iff.
-              break_innermost_match; Z.ltb_to_lt;
-                auto with zarith. }
-            { non_arith_t; Z.ltb_to_lt; reflexivity. }
+            all: [ > idtac "WARNING: Remaining goal:"; print_context_and_goal () .. ].
+          Qed.
+
+          Lemma interp_related_and_Proper {t} (idc : ident t) : interp_is_related_and_Proper idc.
+          Proof using Type.
+            destruct (type.is_not_higher_order_than 3 t) eqn:Hho.
+            { apply type.related_hetero_impl_related_hetero_and_Proper_eqv_not_higher_order_than_3.
+              all: try apply interp_related.
+              all: try apply ident.interp_Proper.
+              all: try apply ZRange.ident.option.interp_Proper.
+              all: try assumption.
+              all: try reflexivity. }
+            { destruct idc.
+              all: try (apply Bool.diff_true_false in Hho; exfalso; exact Hho).
+              (** For command-line debugging, we display goals that should not remain *)
+              all: [ > idtac "WARNING: Remaining goal of order > 3:"; print_context_and_goal () .. ]. }
           Qed.
         End interp_related.
       End option.
diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v
index 5df6d6a5e7..4d21680e4e 100644
--- a/src/BoundsPipeline.v
+++ b/src/BoundsPipeline.v
@@ -1375,7 +1375,7 @@ Module Pipeline.
               let e' := fresh "e" in
               destruct v as [e'|e'] eqn:H;
               cbv beta iota in Hrv;
-              [ apply CheckedPartialEvaluateWithBounds_Correct in H;
+              [ apply CheckedPartialEvaluateWithBounds_Correct_first_order in H;
                 [ let Hwf' := fresh "Hwf" in
                   rewrite (correct_of_final_iff_correct_of_initial Hinterp) in H by assumption;
                   destruct H as [? Hwf']; split_and;