diff --git a/src/AbstractInterpretation/ZRange.v b/src/AbstractInterpretation/ZRange.v
index 7e61de8c8e..a2cdff28bb 100644
--- a/src/AbstractInterpretation/ZRange.v
+++ b/src/AbstractInterpretation/ZRange.v
@@ -536,13 +536,17 @@ Module Compilers.
              | ident.Nat_pred as idc
                => option_map (ident.interp idc)
              | ident.Z_of_nat as idc
-               => option_map (fun n => r[Z.of_nat n~>Z.of_nat n]%zrange)
+             | ident.Z_pos as idc
+               => option_map (fun n => r[ident.interp idc n~>ident.interp idc n]%zrange)
              | ident.Z_to_nat as idc
+             | ident.Z_to_pos as idc
                => fun v => v <- to_literal v; Some (ident.interp idc v)
              | ident.List_length _
                => option_map (@List.length _)
              | ident.value_barrier
                => fun x => x
+             | ident.Pos_mul as idc
+             | ident.Pos_add as idc
              | ident.Nat_max as idc
              | ident.Nat_mul as idc
              | ident.Nat_add as idc
@@ -675,18 +679,22 @@ Module Compilers.
                          n
                    | None => ZRange.type.base.option.None
                    end
-             | ident.nat_rect_arrow _ _
-             | ident.eager_nat_rect_arrow _ _
-               => fun O_case S_case n v
-                 => match n with
+             | ident.nat_rect_arrow _ _ as idc
+             | ident.eager_nat_rect_arrow _ _ as idc
+               (*
+             | ident.nat_rect_fbb_b _ _ _ as idc
+             | ident.nat_rect_fbb_b_b _ _ _ _ as idc
+                *)
+               => fun O_case S_case n
+                  => let t := ((fun t (idc : ident (_ -> _ -> _ -> t)) => t) _ idc) in
+                   match n return type.option.interp t with
                    | Some n
                      => nat_rect
                          _
                          O_case
                          (fun n' rec => S_case (Some n') rec)
                          n
-                         v
-                   | None => ZRange.type.base.option.None
+                   | None => ZRange.type.option.None
                    end
              | ident.list_rect _ _
              | ident.eager_list_rect _ _
@@ -700,18 +708,25 @@ Module Compilers.
                          ls
                    | None => ZRange.type.base.option.None
                    end
-             | ident.list_rect_arrow _ _ _
-             | ident.eager_list_rect_arrow _ _ _
-               => fun N C ls v
-                 => match ls with
+             | ident.list_rect_arrow _ _ _ as idc
+             | ident.eager_list_rect_arrow _ _ _ as idc
+               (*
+             | ident.list_rect_fbb_b _ _ _ _ as idc
+             | ident.list_rect_fbb_b_b _ _ _ _ _ as idc
+             | ident.list_rect_fbb_b_b_b _ _ _ _ _ _ as idc
+             | ident.list_rect_fbb_b_b_b_b _ _ _ _ _ _ _ as idc
+             | ident.list_rect_fbb_b_b_b_b_b _ _ _ _ _ _ _ _ as idc
+                *)
+               => fun N C ls
+                 => let t := ((fun t (idc : ident (_ -> _ -> _ -> t)) => t) _ idc) in
+                   match ls return type.option.interp t with
                    | Some ls
                      => list_rect
                          _
                          N
                          (fun x xs rec => C x (Some xs) rec)
                          ls
-                         v
-                   | None => ZRange.type.base.option.None
+                   | None => ZRange.type.option.None
                    end
              | ident.list_case _ _
                => fun N C ls
@@ -763,6 +778,8 @@ Module Compilers.
              | ident.Z_log2 as idc
              | ident.Z_log2_up as idc
                => fun x => x <- x; Some (ZRange.two_corners (ident.interp idc) x)
+             | ident.Z_abs as idc
+               => fun x => x <- x; Some (ZRange.two_corners_and_zero (ident.interp idc) x)
              | ident.Z_max as idc
              | ident.Z_min as idc
              | ident.Z_add as idc
diff --git a/src/AbstractInterpretation/ZRangeCommonProofs.v b/src/AbstractInterpretation/ZRangeCommonProofs.v
index 1a6992810b..2fb7f87210 100644
--- a/src/AbstractInterpretation/ZRangeCommonProofs.v
+++ b/src/AbstractInterpretation/ZRangeCommonProofs.v
@@ -9,6 +9,7 @@ Require Import Crypto.Util.NatUtil.
 Require Import Crypto.Util.ZUtil.Morphisms.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.Tactics.DestructHead.
+Require Import Crypto.Util.Tactics.DoWithHyp.
 Require Import Crypto.AbstractInterpretation.ZRange.
 
 Module Compilers.
@@ -36,6 +37,14 @@ Module Compilers.
                            | progress inversion_option
                            | discriminate
                            | solve [ eauto ]
+                           | apply (@list_rect_Proper_gen _ ((_ -> _) -> _ -> _ -> _ -> _ -> _) ((eq ==> eq) ==> eq ==> eq ==> eq ==> eq ==> eq)%signature)
+                           | apply (@list_rect_Proper_gen _ ((_ -> _) -> _ -> _ -> _ -> _) ((eq ==> eq) ==> eq ==> eq ==> eq ==> eq)%signature)
+                           | apply (@list_rect_Proper_gen _ ((_ -> _) -> _ -> _ -> _) ((eq ==> eq) ==> eq ==> eq ==> eq)%signature)
+                           | apply (@list_rect_Proper_gen _ ((_ -> _) -> _ -> _) ((eq ==> eq) ==> eq ==> eq)%signature)
+                           | apply (@list_rect_Proper_gen _ ((_ -> _) -> _) ((eq ==> eq) ==> eq)%signature)
+                           | apply (@nat_rect_Proper_nondep_gen ((_ -> _) -> _ -> _) ((eq ==> eq) ==> eq ==> eq)%signature)
+                           | apply (@nat_rect_Proper_nondep_gen ((_ -> _) -> _) ((eq ==> eq) ==> eq)%signature)
+                           | apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature)
                            | apply NatUtil.nat_rect_Proper_nondep
                            | apply ListUtil.list_rect_Proper
                            | apply ListUtil.list_rect_arrow_Proper
@@ -43,7 +52,6 @@ Module Compilers.
                            | apply ListUtil.pointwise_map
                            | apply ListUtil.fold_right_Proper
                            | apply ListUtil.update_nth_Proper
-                           | apply (@nat_rect_Proper_nondep_gen (_ -> _) (eq ==> eq)%signature)
                            | cbn; apply (f_equal (@Some _))
                            | progress cbn [ZRange.ident.option.interp]
                            | progress cbv [zrange_rect]
@@ -54,7 +62,8 @@ Module Compilers.
                              | [ H : forall x y, x = y -> _ |- _ ] => specialize (fun x => H x x eq_refl)
                              | [ H : forall x, ?f x = ?g x, H1 : ?f ?y = _, H2 : ?g ?y = _ |- _ ]
                                => specialize (H y); rewrite H1, H2 in H
-                             end ].
+                             end
+                           | do_with_exactly_one_hyp ltac:(fun H => apply H; clear H) ].
           Qed.
         End interp_related.
       End option.
diff --git a/src/AbstractInterpretation/ZRangeProofs.v b/src/AbstractInterpretation/ZRangeProofs.v
index aad9dd774c..a109f24723 100644
--- a/src/AbstractInterpretation/ZRangeProofs.v
+++ b/src/AbstractInterpretation/ZRangeProofs.v
@@ -436,7 +436,7 @@ Module Compilers.
                          | break_innermost_match_step
                          | break_innermost_match_hyps_step
                          | progress cbn [id
-                                           ZRange.type.base.option.is_bounded_by is_bounded_by_bool ZRange.type.base.is_bounded_by lower upper fst snd projT1 projT2 bool_eq base.interp base.base_interp Crypto.Util.Option.bind fold_andb_map negb ZRange.ident.option.to_literal ZRange.type.base.option.None fst snd ZRange.type.base.option.interp ZRange.type.base.interp List.combine List.In base.interp_beq base.base_interp_beq base.base_interp] in *
+                                           ZRange.type.base.option.is_bounded_by is_bounded_by_bool ZRange.type.base.is_bounded_by lower upper fst snd projT1 projT2 bool_eq base.interp base.base_interp Crypto.Util.Option.bind fold_andb_map negb ZRange.ident.option.to_literal ZRange.type.base.option.None fst snd ZRange.type.base.option.interp ZRange.type.base.interp List.combine List.In base.interp_beq base.base_interp_beq base.base_interp ZRange.type.option.None] in *
                          | progress ident.fancy.cbv_fancy_in_all
                          | progress destruct_head'_bool
                          | solve [ auto with nocore ]
@@ -482,16 +482,43 @@ Module Compilers.
                            | [ |- and _ _ ] => apply conj
                            end
                          | progress cbv [bool_eq Bool.eqb option_map List.nth_default Definitions.Z.bneg is_bounded_by_bool zrange_beq] in *
+                         | let rec do_rect_head lhs rhs k :=
+                             lazymatch lhs with
+                             | nat_rect ?P ?O ?S ?n
+                               => lazymatch rhs with
+                                  | nat_rect ?P' ?O' ?S' n
+                                    => is_var n;
+                                       k ();
+                                       induction n; cbn [nat_rect];
+                                       generalize dependent (nat_rect P O S); generalize dependent (nat_rect P' O' S');
+                                       intros
+                                  end
+                             | list_rect ?P ?N ?C ?ls
+                               => lazymatch rhs with
+                                  | list_rect ?P' ?N' ?C' ?ls'
+                                    => lazymatch goal with
+                                       | [ H : length ls = length ls' |- _ ]
+                                         => is_var ls; is_var ls'; k ();
+                                            let IH := fresh "IH" in
+                                            (revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; intros; cbn [list_rect length] in * );
+                                            [
+                                            | exfalso; discriminate | exfalso; discriminate
+                                            | specialize (IH ls');
+                                              generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ];
+                                            intros
+                                       end
+                                  end
+                             | ?f ?x
+                               => lazymatch rhs with
+                                  | ?g ?y
+                                    => is_var x; is_var y;
+                                       do_rect_head f g ltac:(fun _ => k (); revert dependent x; try revert dependent y)
+                                  end
+                             end in
+                           lazymatch goal with
+                           | [ |- ?R ?lhs ?rhs = true ] => do_rect_head lhs rhs ltac:(fun _ => idtac)
+                           end
                          | match goal with
-                           | [ |- ?R (nat_rect ?P ?O ?S ?n) (nat_rect ?P' ?O' ?S' ?n) = true ]
-                             => is_var n; induction n; cbn [nat_rect];
-                                generalize dependent (nat_rect P O S); generalize dependent (nat_rect P' O' S');
-                                intros
-                           | [ |- ?R (nat_rect ?P ?O ?S ?n ?x) (nat_rect ?P' ?O' ?S' ?n ?y) = true ]
-                             => is_var n; is_var x; is_var y;
-                                revert dependent x; revert dependent y; induction n; cbn [nat_rect];
-                                generalize dependent (nat_rect P O S); generalize dependent (nat_rect P' O' S');
-                                intros
                            | [ H : length ?ls = length ?ls' |- ?R (List.fold_right ?f ?x ?ls) (List.fold_right ?f' ?x' ?ls') = true ]
                              => is_var ls; is_var ls';
                                 let IH := fresh "IH" in
@@ -510,25 +537,6 @@ Module Compilers.
                                  | specialize (IH ls');
                                    generalize dependent (List.fold_right f x); generalize dependent (List.fold_right f' x') ];
                                 intros
-                           | [ H : length ?ls = length ?ls' |- ?R (list_rect ?P ?N ?C ?ls) (list_rect ?P' ?N' ?C' ?ls') = true ]
-                             => is_var ls; is_var ls';
-                                let IH := fresh "IH" in
-                                revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; intros; cbn [list_rect length] in *;
-                                [
-                                 | exfalso; discriminate | exfalso; discriminate
-                                 | specialize (IH ls');
-                                   generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ];
-                                intros
-                           | [ H : length ?ls = length ?ls' |- ?R (list_rect ?P ?N ?C ?ls ?x) (list_rect ?P' ?N' ?C' ?ls' ?y) = true ]
-                             => is_var ls; is_var ls'; is_var x; is_var y;
-                                revert dependent y; try revert dependent x;
-                                let IH := fresh "IH" in
-                                revert dependent ls'; induction ls as [|? ls IH]; intros [|? ls']; intros; cbn [list_rect length] in *;
-                                [
-                                | exfalso; discriminate | exfalso; discriminate
-                                | specialize (IH ls');
-                                  generalize dependent (list_rect P N C); generalize dependent (list_rect P' N' C') ];
-                                intros
                            | [ H : forall a b, ?R a b = true -> ?R' (?f a) (?g b) = true |- ?R' (?f _) (?g _) = true ] => apply H; clear H
                            | [ H : forall a b, ?R a b = true -> forall c d, ?R' c d = true -> ?R'' (?f a c) (?g b d) = true |- ?R'' (?f _ _) (?g _ _) = true ]
                              => apply H; clear H
@@ -550,7 +558,8 @@ Module Compilers.
                              => apply ZRange.type.base.option.is_bounded_by_union_l
                            | [ |- ZRange.type.base.option.is_bounded_by (ZRange.type.base.option.union _ _) (Bool.bool_rect_nodep _ _ false) = true ]
                              => apply ZRange.type.base.option.is_bounded_by_union_r
-                           end ].
+                           end
+                         | do_with_hyp' ltac:(fun H => apply H; clear H; now non_arith_t) ].
 
           Local Lemma mul_by_halves_bounds x y n :
             (0 <= x < 2^ (n / 2))%Z ->
@@ -723,6 +732,15 @@ Module Compilers.
             all: change (@list_rect_arrow_nodep) with (fun A P Q => @list_rect A (fun _ => P -> Q)).
             all: change (@Thunked.list_case) with (fun A P PNil => @list_case A (fun _ => P) (PNil Datatypes.tt)) in *.
             all: change (@Thunked.option_rect) with (fun A P PS PN => @option_rect A (fun _ => P) PS (PN Datatypes.tt)) in *.
+            all: cbv [
+                     nat_rect_fbb_b
+                       nat_rect_fbb_b_b
+                       list_rect_fbb_b
+                       list_rect_fbb_b_b
+                       list_rect_fbb_b_b_b
+                       list_rect_fbb_b_b_b_b
+                       list_rect_fbb_b_b_b_b_b
+                   ] in *.
             all: cbv [respectful_hetero option_map option_rect zrange_rect list_case].
             all: intros.
             all: destruct_head_hnf' prod.
@@ -786,6 +804,9 @@ Module Compilers.
                         | [ Hx : is_bounded_by_bool _ ?x = true
                             |- is_bounded_by_bool _ (ZRange.two_corners ?f ?x) = true ]
                           => apply (fun pf => @ZRange.monotoneb_two_corners_gen f pf x _ Hx); intros; auto with zarith
+                        | [ Hx : is_bounded_by_bool _ ?x = true
+                            |- is_bounded_by_bool _ (ZRange.two_corners_and_zero ?f ?x) = true ]
+                          => apply (fun pf1 pf2 => @ZRange.monotoneb_two_corners_and_zero_gen f pf1 pf2 x _ Hx); intros; auto with zarith
                         | [ |- is_bounded_by_bool (if _ then _ else _) (ZRange.four_corners _ _ _) = true ]
                           => apply ZRange.is_bounded_by_bool_Proper_if_bool_union_dep; intros; Z.ltb_to_lt
                         | [ _ : is_bounded_by_bool ?x1 ?r1 = true,
@@ -817,6 +838,7 @@ Module Compilers.
                              end
                            | intros; mul_by_halves_t ].
             all: try solve [ non_arith_t; Z.ltb_to_lt; reflexivity ].
+            all: try solve [ non_arith_t; try match goal with |- ?x = true => destruct x eqn:? end; reflect_hyps; subst; nia ].
             all: try solve [ cbv [ZRange.ToConstant.four_corners ZRange.ToConstant.Option.four_corners ZRange.ToConstant.Option.apply_to_range ZRange.ToConstant.Option.two_corners ZRange.ToConstant.Option.union option_beq Bool.eqb] in *; non_arith_t; Z.ltb_to_lt; lia ].
             (** For command-line debugging, we display goals that should not remain *)
             all: [ > idtac "WARNING: Remaining goal:"; print_context_and_goal () .. ].
@@ -831,11 +853,221 @@ Module Compilers.
               all: try apply ZRange.ident.option.interp_Proper.
               all: try assumption.
               all: try reflexivity. }
-            { destruct idc.
+            { (*
+              pose proof (interp_related idc) as Hir.
+              pose proof (ident.interp_Proper idc idc eq_refl) as Hip.
+              pose proof (ZRange.ident.option.interp_Proper assume_cast_truncates idc idc eq_refl) as Hzip.
+               *)
+              destruct idc.
               all: try (apply Bool.diff_true_false in Hho; exfalso; exact Hho).
+              (*
+              all: cbn [interp_is_related_and_Proper type.interp type.related interp_is_related] in *;
+                cbv [Proper respectful respectful_hetero] in *.
+              all: cbn [ZRange.ident.option.interp ident.interp].
+              all: cbn [ZRange.type.base.option.interp ZRange.type.option.None ZRange.type.base.interp].
+              all: cbn [base.interp IdentifiersBasicGENERATED.Compilers.base_interp].
+              all: cbv [
+                       nat_rect_fbb_b
+                         nat_rect_fbb_b_b
+                         list_rect_fbb_b
+                         list_rect_fbb_b_b
+                         list_rect_fbb_b_b_b
+                         list_rect_fbb_b_b_b_b
+                         list_rect_fbb_b_b_b_b_b
+                     ] in *.
+              all: cbn [Language.Compilers.base.interp IdentifiersBasicGENERATED.Compilers.base_interp ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by base.interp_beq].
+              all: lazymatch goal with
+                   | [ |- (forall (a1 : ?A1) (a2 : @?A2 a1) (a3 : @?A3 a1 a2) (a4 : @?A4 a1 a2 a3) (a5 : @?A5 a1 a2 a3 a4) (a6 : @?A6 a1 a2 a3 a4 a5) (a7 a8 : ?optT) (a9 : a7 = a8), @?AP a1 a2 a4 a5 a7 a8)
+                          /\ (forall (b1 : ?B1) (b2 : @?B2 b1) (b3 : @?B3 b1 b2) (b4 : @?B4 b1 b2 b3) (b5 : @?B5 b1 b2 b3 b4) (b6 : @?B6 b1 b2 b3 b4 b5) (b7 b8 : ?T) (b9 : b7 = b8), @?BP b1 b2 b4 b5 b7 b8)
+                          /\ (forall (c1 : ?C1) (c2 : @?C2 c1) (c3 : @?C3 c1 c2),
+                                 (forall (d4 : @?D4 c1 c2 c3) (d5 : @?D5 c1 c2 c3 d4) (d6 : @?D6 c1 c2 c3 d4 d5) (d7 d8 : ?optT) (d9 : d7 = d8), @?DP c1 c2 d4 d5 d7 d8)
+                                 /\ (forall (e4 : @?E4 c1 c2 c3) (e5 : @?E5 c1 c2 c3 e4) (e6 : @?E6 c1 c2 c3 e4 e5) (e7 e8 : ?T) (e9 : e7 = e8), @?EP c1 c2 e4 e5 e7 e8)
+                                 /\ (forall (f4 : @?F4 c1 c2 c3) (f5 : @?F5 c1 c2 c3 f4) (f6 : @?F6 c1 c2 c3 f4 f5),
+                                        (forall (g7 g8 : ?optT) (g9 : g7 = g8), @?GP c1 c2 f4 f5 g7 g8)
+                                        /\ (forall (h7 h8 : ?T) (h9 : h7 = h8), @?HP c1 c2 f4 f5 h7 h8)
+                                        /\ (forall (i7 : ?optT) (i8 : ?T) (i9 : @?TR i7 i8), @?IP c1 c2 f4 f5 i7 i8))) ]
+                     => let G'
+                          := constr:(forall (i7 : optT) (i8 : T),
+                                        (forall (a1 : A1) (a2 : A2 a1) (a3 : A3 a1 a2) (a4 : A4 a1 a2 a3) (a5 : A5 a1 a2 a3 a4) (a6 : A6 a1 a2 a3 a4 a5), AP a1 a2 a4 a5 i7 i7)
+                                        /\ (forall (b1 : B1) (b2 : B2 b1) (b3 : B3 b1 b2) (b4 : B4 b1 b2 b3) (b5 : B5 b1 b2 b3 b4) (b6 : B6 b1 b2 b3 b4 b5), BP b1 b2 b4 b5 i8 i8)
+                                        /\ (forall (c1 : C1) (c2 : C2 c1) (c3 : C3 c1 c2),
+                                               (forall (d4 : D4 c1 c2 c3) (d5 : D5 c1 c2 c3 d4) (d6 : D6 c1 c2 c3 d4 d5), DP c1 c2 d4 d5 i7 i7)
+                                               /\ (forall (e4 : E4 c1 c2 c3) (e5 : E5 c1 c2 c3 e4) (e6 : E6 c1 c2 c3 e4 e5), EP c1 c2 e4 e5 i8 i8)
+                                               /\ (forall (f4 : F4 c1 c2 c3) (f5 : F5 c1 c2 c3 f4) (f6 : F6 c1 c2 c3 f4 f5),
+                                                      GP c1 c2 f4 f5 i7 i7
+                                                      /\ HP c1 c2 f4 f5 i8 i8
+                                                      /\ (TR i7 i8 -> IP c1 c2 f4 f5 i7 i8)))) in
+                        cut G';
+                        [ clear;
+                          change (G'
+                                  -> ((forall (a1 : A1) (a2 : A2 a1) (a3 : A3 a1 a2) (a4 : A4 a1 a2 a3) (a5 : A5 a1 a2 a3 a4) (a6 : A6 a1 a2 a3 a4 a5) (a7 a8 : optT) (a9 : a7 = a8), AP a1 a2 a4 a5 a7 a8)
+                                      /\ (forall (b1 : B1) (b2 : B2 b1) (b3 : B3 b1 b2) (b4 : B4 b1 b2 b3) (b5 : B5 b1 b2 b3 b4) (b6 : B6 b1 b2 b3 b4 b5) (b7 b8 : T) (b9 : b7 = b8), BP b1 b2 b4 b5 b7 b8)
+                                      /\ (forall (c1 : C1) (c2 : C2 c1) (c3 : C3 c1 c2),
+                                             (forall (d4 : D4 c1 c2 c3) (d5 : D5 c1 c2 c3 d4) (d6 : D6 c1 c2 c3 d4 d5) (d7 d8 : optT) (d9 : d7 = d8), DP c1 c2 d4 d5 d7 d8)
+                                             /\ (forall (e4 : E4 c1 c2 c3) (e5 : E5 c1 c2 c3 e4) (e6 : E6 c1 c2 c3 e4 e5) (e7 e8 : T) (e9 : e7 = e8), EP c1 c2 e4 e5 e7 e8)
+                                             /\ (forall (f4 : F4 c1 c2 c3) (f5 : F5 c1 c2 c3 f4) (f6 : F6 c1 c2 c3 f4 f5),
+                                                    (forall (g7 g8 : optT) (g9 : g7 = g8), GP c1 c2 f4 f5 g7 g8)
+                                                    /\ (forall (h7 h8 : T) (h9 : h7 = h8), HP c1 c2 f4 f5 h7 h8)
+                                                    /\ (forall (i7 : optT) (i8 : T) (i9 : TR i7 i8), IP c1 c2 f4 f5 i7 i8)))));
+                          intro H'; revert H';
+                          try generalize AP BP DP EP GP HP IP;
+                          try generalize optT T;
+                          try generalize F6;
+                          try generalize E6;
+                          try generalize D6;
+                          try generalize C3;
+                          try generalize B3 B6;
+                          try generalize A3 A6;
+                          intros
+                        | shelve ]
+                   | _ => (** For command-line debugging, we display goals that should not remain *)
+                       idtac "WARNING: Remaining goal of order > 3:"; print_context_and_goal ();
+                       shelve
+                   end.
+              all: repeat split; repeat intro; subst; eapply H'.
+              all: try eassumption.
+              all: try reflexivity.
+              all: try solve [ constructor ].
+              all: fail.
+              Unshelve.
+              all: cbv beta.
+              Time
+                all: intros [x|] y;
+              [ revert x; induction y; cbn [nat_rect list_rect];
+                [ intro x; induction x; cbn [nat_rect list_rect];
+                  [ solve [
+                        repeat split; intros;
+                        auto;
+                        repeat first [ do_with_exactly_one_hyp ltac:(fun H => apply H; clear H)
+                                     | reflexivity ]
+                      ]
+                  | pose 1 as GOAL ]
+                | intro x;
+                  repeat match goal with
+                    | [ y : ?T |- _ ]
+                      => lazymatch T with
+                         | nat => idtac
+                         | list _ => idtac
+                         end;
+                  tryif constr_eq y x then fail else revert dependent y
+                  end;
+                  induction x; cbn [nat_rect list_rect];
+                  [ pose 2 as GOAL
+                  | pose 3 as GOAL ] ]
+              | induction y; cbn [nat_rect list_rect];
+                [ repeat split; intros; auto;
+                  solve [
+                      repeat first [ lazymatch goal with
+                                     | [ |- ZRange.type.base.option.is_bounded_by ZRange.type.base.option.None _ = true ]
+                                       => apply type.base.option.is_bounded_by_None
+                                     end
+                                   | do_with_exactly_one_hyp ltac:(fun H => apply H; clear H)
+                                   | reflexivity ]
+                    ]
+                | pose 4 as GOAL ]
+              ].
+              Time
+                all:
+                lazymatch goal with
+                | [ GOAL := 1 |- _ ]
+                  => try time (repeat split; intros; auto;
+                               reflect_hyps; destruct_head'_False;
+                               solve [
+                                   repeat first [ do_with_hyp' ltac:(fun H => solve [ apply H; auto ])
+                                                | do_with_exactly_one_hyp ltac:(fun H => apply H); intros; auto
+                                                | reflexivity
+                                                | solve [ auto ]
+                                                | progress subst
+                                                | progress intros ]
+                                 ]
+                       )
+                | _ => idtac
+                end.
+              Time
+                all:
+                lazymatch goal with
+                | [ GOAL := 4 |- _ ]
+                  => try time
+                         (repeat split; intros; auto;
+                          let rec go _ :=
+                            repeat first [ lazymatch goal with
+                                           | [ |- ZRange.type.base.option.is_bounded_by ZRange.type.base.option.None _ = true ]
+                                             => apply type.base.option.is_bounded_by_None
+                                           end
+                                         | do_with_hyp' ltac:(fun H => solve [ apply H; auto ])
+                                         | do_with_exactly_one_hyp ltac:(fun H => apply H); auto; intros
+                                         | reflexivity
+                                         | solve [ auto ]
+                                         | progress subst
+                                         | progress intros
+                                         | do_with_hyp' ltac:(fun H => apply H; solve [ go () ]) ] in
+                          solve [ go () ])
+                | _ => idtac
+                end.
+              Time
+                all:
+                lazymatch goal with
+                | [ GOAL := 2 |- _ ]
+                  => try time
+                       (repeat split; intros; auto;
+                        reflect_hyps; destruct_head'_False;
+                        solve [
+                            repeat first [ do_with_hyp' ltac:(fun H => solve [ apply H; auto ])
+                                         | do_with_exactly_one_hyp ltac:(fun H => apply H); intros; auto
+                                         | reflexivity
+                                         | solve [ auto ]
+                                         | solve [ constructor ]
+                                         | progress subst
+                                         | progress intros ]
+                          ]
+                       )
+                | _ => idtac
+                end.
+              Time
+                all:
+                lazymatch goal with
+                | [ GOAL := 3 |- _ ]
+                  => try time
+                       (repeat split; intros; auto;
+                        let rec go _ :=
+                          repeat first [ do_with_hyp' ltac:(fun H => solve [ apply H; auto ])
+                                       | do_with_exactly_one_hyp ltac:(fun H => apply H); auto; intros
+                                       | reflexivity
+                                       | solve [ auto ]
+                                       | solve [ constructor ]
+                                       | progress subst
+                                       | progress intros
+                                       | do_with_hyp' ltac:(fun H => apply H; solve [ go () ]) ] in
+                        solve [ go () ])
+                | _ => idtac
+                end.
+              Time
+                all:
+                lazymatch goal with
+                | [ GOAL := 3 |- _ ]
+                  => try time
+                       (repeat split; intros; auto;
+                        cbn [fold_andb_map] in *;
+                        lazymatch goal with
+                        | [ H : andb _ _ = true |- _ ] => rewrite Bool.andb_true_iff in H; destruct H
+                        | _ => idtac
+                        end;
+                        let rec go _ :=
+                          repeat first [ do_with_hyp' ltac:(fun H => solve [ apply H; auto ])
+                                       | do_with_exactly_one_hyp ltac:(fun H => apply H); auto; intros
+                                       | reflexivity
+                                       | solve [ auto ]
+                                       | solve [ constructor ]
+                                       | progress subst
+                                       | progress intros
+                                       | do_with_hyp' ltac:(fun H => apply H; solve [ go () ]) ] in
+                        solve [ go () ])
+                | _ => idtac
+                end.
+               *)
               (** For command-line debugging, we display goals that should not remain *)
               all: [ > idtac "WARNING: Remaining goal of order > 3:"; print_context_and_goal () .. ]. }
-          Qed.
+          Time Qed.
         End interp_related.
       End option.
     End ident.
diff --git a/src/Assembly/Equivalence.v b/src/Assembly/Equivalence.v
index 5acc755847..07f93c8808 100644
--- a/src/Assembly/Equivalence.v
+++ b/src/Assembly/Equivalence.v
@@ -1042,26 +1042,12 @@ Proof.
           | ident.Literal base.type.Z v
             => App (const v, nil)
           | ident.Z_add => fun x y => App (addZ, [x; y])
-
-          | ident.Z_modulo
-            => symex_T_error (Unhandled_identifier idc)
           | ident.Z_mul => fun x y => App (mulZ, [x; y])
-          | ident.Z_pow
-            => symex_T_error (Unhandled_identifier idc)
           | ident.Z_sub => fun x y => y' <- App (negZ, [y]); App (addZ, [x;y'])
-          | ident.Z_opp
-          | ident.Z_div
-          | ident.Z_log2
-          | ident.Z_log2_up
-          | ident.Z_to_nat
-            => symex_T_error (Unhandled_identifier idc)
           | ident.Z_shiftr => fun x y => App (shrZ, [x; y])
           | ident.Z_shiftl => fun x y => App (shlZ, [x; y])
           | ident.Z_land => fun x y => App (andZ, [x; y])
           | ident.Z_lor => fun x y => App (orZ, [x; y])
-          | ident.Z_min
-          | ident.Z_max
-            => symex_T_error (Unhandled_identifier idc)
           | ident.Z_mul_split => fun bs x y =>
             vs <- RevealWidth bs; s <- App (const (Z.of_N vs), nil);
             v <- App (mulZ, [x; y]);
@@ -1096,21 +1082,10 @@ Proof.
             a <- App (add s, [x;y';z']);
             c <- App (subborrowZ s, [x;y;z]);
             symex_return (a, c)
-          | ident.Z_ltz
-            => symex_T_error (Unhandled_identifier idc)
           | ident.Z_zselect => fun c x y => App (Symbolic.selectznz, [c; x; y])
-          | ident.Z_add_modulo
-            => symex_T_error (Unhandled_identifier idc)
           | ident.Z_truncating_shiftl => fun s x y =>
             s <- RevealConstant s;
             App (shl s, [x; y])
-          | ident.Z_bneg
-          | ident.Z_lnot_modulo
-          | ident.Z_lxor
-          | ident.Z_rshi
-          | ident.Z_cc_m
-          | ident.Z_combine_at_bitwidth
-            => symex_T_error (Unhandled_identifier idc)
 
           | ident.comment _
           | ident.comment_no_keep _
@@ -1119,11 +1094,6 @@ Proof.
             => fun v => symex_return v
           | ident.tt
             => symex_return tt
-          | ident.Literal base.type.bool _ as idc
-          | ident.Literal base.type.string _ as idc
-          | ident.None _ as idc
-          | ident.Some _ as idc
-            => symex_T_error (Unhandled_identifier idc)
           | ident.Literal base.type.zrange v
           | ident.Literal base.type.nat v
             => symex_return v
@@ -1176,6 +1146,29 @@ Proof.
           | ident.Z_of_nat
             => fun n => App (const (Z.of_nat n), nil)
 
+          | ident.Z_modulo
+          | ident.Z_pow
+          | ident.Z_opp
+          | ident.Z_div
+          | ident.Z_log2
+          | ident.Z_log2_up
+          | ident.Z_to_nat
+          | ident.Z_min
+          | ident.Z_max
+          | ident.Z_abs
+          | ident.Z_ltz
+          | ident.Z_add_modulo
+          | ident.Z_bneg
+          | ident.Z_lnot_modulo
+          | ident.Z_lxor
+          | ident.Z_rshi
+          | ident.Z_cc_m
+          | ident.Z_combine_at_bitwidth
+          | ident.Literal base.type.bool _
+          | ident.Literal base.type.string _
+          | ident.Literal base.type.positive _
+          | ident.None _
+          | ident.Some _
           | ident.Z_eqb
           | ident.Z_leb
           | ident.Z_ltb
@@ -1194,6 +1187,15 @@ Proof.
           | ident.eager_list_rect _ _
           | ident.list_rect_arrow _ _ _
           | ident.eager_list_rect_arrow _ _ _
+          (*
+          | ident.nat_rect_fbb_b _ _ _
+          | ident.nat_rect_fbb_b_b _ _ _ _
+          | ident.list_rect_fbb_b _ _ _ _
+          | ident.list_rect_fbb_b_b _ _ _ _ _
+          | ident.list_rect_fbb_b_b_b _ _ _ _ _ _
+          | ident.list_rect_fbb_b_b_b_b _ _ _ _ _ _ _
+          | ident.list_rect_fbb_b_b_b_b_b _ _ _ _ _ _ _ _
+           *)
           | ident.list_case _ _
           | ident.List_map _ _
           | ident.List_flat_map _ _
@@ -1203,6 +1205,10 @@ Proof.
           | ident.List_update_nth _
           | ident.option_rect _ _
           | ident.zrange_rect _
+          | ident.Pos_add
+          | ident.Pos_mul
+          | ident.Z_pos
+          | ident.Z_to_pos
           | ident.fancy_add
           | ident.fancy_addc
           | ident.fancy_sub
diff --git a/src/BoundsPipeline.v b/src/BoundsPipeline.v
index 5df6d6a5e7..5666bb1945 100644
--- a/src/BoundsPipeline.v
+++ b/src/BoundsPipeline.v
@@ -459,6 +459,7 @@ Module Pipeline.
          | base.type.unit
            => fun 'tt 'tt => (false, nil, nil)
          | base.type.type_base base.type.nat
+         | base.type.type_base base.type.positive
          | base.type.type_base base.type.bool
          | base.type.type_base base.type.zrange
          | base.type.type_base base.type.string
diff --git a/src/Language/APINotations.v b/src/Language/APINotations.v
index df583c1653..cd6472a763 100644
--- a/src/Language/APINotations.v
+++ b/src/Language/APINotations.v
@@ -81,10 +81,21 @@ Module Compilers.
   Global Arguments ident_nat_rect_arrow {_ _} : assert.
   Global Arguments ident_eager_nat_rect {_} : assert.
   Global Arguments ident_eager_nat_rect_arrow {_ _} : assert.
+  (*
+  Global Arguments ident_nat_rect_fbb_b {_ _ _} : assert.
+  Global Arguments ident_nat_rect_fbb_b_b {_ _ _ _} : assert.
+*)
   Global Arguments ident_list_rect {_ _} : assert.
-  Global Arguments ident_list_rect_arrow {_ _ _} : assert.
   Global Arguments ident_eager_list_rect {_ _} : assert.
   Global Arguments ident_eager_list_rect_arrow {_ _ _} : assert.
+  Global Arguments ident_list_rect_arrow {_ _ _} : assert.
+  (*
+  Global Arguments ident_list_rect_fbb_b {_ _ _ _} : assert.
+  Global Arguments ident_list_rect_fbb_b_b {_ _ _ _ _} : assert.
+  Global Arguments ident_list_rect_fbb_b_b_b {_ _ _ _ _ _} : assert.
+  Global Arguments ident_list_rect_fbb_b_b_b_b {_ _ _ _ _ _ _} : assert.
+  Global Arguments ident_list_rect_fbb_b_b_b_b_b {_ _ _ _ _ _ _ _} : assert.
+*)
   Global Arguments ident_list_case {_ _} : assert.
   Global Arguments ident_List_length {_} : assert.
   Global Arguments ident_List_firstn {_} : assert.
@@ -165,6 +176,7 @@ Module Compilers.
       Import IdentifiersBasicGENERATED.Compilers.
       Notation base := base (only parsing).
       Notation Z := Z (only parsing).
+      Notation positive := positive (only parsing).
       Notation nat := nat (only parsing).
       Notation zrange := zrange (only parsing).
       Notation bool := bool (only parsing).
@@ -245,10 +257,21 @@ Module Compilers.
     Notation nat_rect_arrow := Compilers.ident_nat_rect_arrow (only parsing).
     Notation eager_nat_rect := Compilers.ident_eager_nat_rect (only parsing).
     Notation eager_nat_rect_arrow := Compilers.ident_eager_nat_rect_arrow (only parsing).
+    (*
+    Notation nat_rect_fbb_b := Compilers.ident_nat_rect_fbb_b (only parsing).
+    Notation nat_rect_fbb_b_b := Compilers.ident_nat_rect_fbb_b_b (only parsing).
+*)
     Notation list_rect := Compilers.ident_list_rect (only parsing).
     Notation list_rect_arrow := Compilers.ident_list_rect_arrow (only parsing).
     Notation eager_list_rect := Compilers.ident_eager_list_rect (only parsing).
     Notation eager_list_rect_arrow := Compilers.ident_eager_list_rect_arrow (only parsing).
+    (*
+    Notation list_rect_fbb_b := Compilers.ident_list_rect_fbb_b (only parsing).
+    Notation list_rect_fbb_b_b := Compilers.ident_list_rect_fbb_b_b (only parsing).
+    Notation list_rect_fbb_b_b_b := Compilers.ident_list_rect_fbb_b_b_b (only parsing).
+    Notation list_rect_fbb_b_b_b_b := Compilers.ident_list_rect_fbb_b_b_b_b (only parsing).
+    Notation list_rect_fbb_b_b_b_b_b := Compilers.ident_list_rect_fbb_b_b_b_b_b (only parsing).
+*)
     Notation list_case := Compilers.ident_list_case (only parsing).
     Notation List_length := Compilers.ident_List_length (only parsing).
     Notation List_seq := Compilers.ident_List_seq (only parsing).
@@ -266,6 +289,8 @@ Module Compilers.
     Notation List_update_nth := Compilers.ident_List_update_nth (only parsing).
     Notation List_nth_default := Compilers.ident_List_nth_default (only parsing).
     Notation eager_List_nth_default := Compilers.ident_eager_List_nth_default (only parsing).
+    Notation Pos_add := Compilers.ident_Pos_add (only parsing).
+    Notation Pos_mul := Compilers.ident_Pos_mul (only parsing).
     Notation Z_add := Compilers.ident_Z_add (only parsing).
     Notation Z_mul := Compilers.ident_Z_mul (only parsing).
     Notation Z_pow := Compilers.ident_Z_pow (only parsing).
@@ -282,12 +307,15 @@ Module Compilers.
     Notation Z_gtb := Compilers.ident_Z_gtb (only parsing).
     Notation Z_of_nat := Compilers.ident_Z_of_nat (only parsing).
     Notation Z_to_nat := Compilers.ident_Z_to_nat (only parsing).
+    Notation Z_pos := Compilers.ident_Z_pos (only parsing).
+    Notation Z_to_pos := Compilers.ident_Z_to_pos (only parsing).
     Notation Z_shiftr := Compilers.ident_Z_shiftr (only parsing).
     Notation Z_shiftl := Compilers.ident_Z_shiftl (only parsing).
     Notation Z_land := Compilers.ident_Z_land (only parsing).
     Notation Z_lor := Compilers.ident_Z_lor (only parsing).
     Notation Z_min := Compilers.ident_Z_min (only parsing).
     Notation Z_max := Compilers.ident_Z_max (only parsing).
+    Notation Z_abs := Compilers.ident_Z_abs (only parsing).
     Notation Z_bneg := Compilers.ident_Z_bneg (only parsing).
     Notation Z_lnot_modulo := Compilers.ident_Z_lnot_modulo (only parsing).
     Notation Z_lxor := Compilers.ident_Z_lxor (only parsing).
diff --git a/src/Language/IdentifierParameters.v b/src/Language/IdentifierParameters.v
index 66aa4b36bc..3876026ac3 100644
--- a/src/Language/IdentifierParameters.v
+++ b/src/Language/IdentifierParameters.v
@@ -80,6 +80,7 @@ Definition var_like_idents : InductiveHList.hlist
 
 Definition base_type_list_named : InductiveHList.hlist
   := [with_name Z BinInt.Z
+      ; with_name positive BinPos.positive
       ; with_name bool Datatypes.bool
       ; with_name nat Datatypes.nat
       ; with_name zrange ZRange.zrange
@@ -110,10 +111,21 @@ Definition all_ident_named_interped : InductiveHList.hlist
       ; with_name ident_eager_nat_rect (ident.eagerly (@Thunked.nat_rect))
       ; with_name ident_nat_rect_arrow (@nat_rect_arrow_nodep)
       ; with_name ident_eager_nat_rect_arrow (ident.eagerly (@nat_rect_arrow_nodep))
+                  (*
+      ; with_name ident_nat_rect_fbb_b (@nat_rect_fbb_b)
+      ; with_name ident_nat_rect_fbb_b_b (@nat_rect_fbb_b_b)
+*)
       ; with_name ident_list_rect (@Thunked.list_rect)
       ; with_name ident_eager_list_rect (ident.eagerly (@Thunked.list_rect))
       ; with_name ident_list_rect_arrow (@list_rect_arrow_nodep)
       ; with_name ident_eager_list_rect_arrow (ident.eagerly (@list_rect_arrow_nodep))
+                  (*
+      ; with_name ident_list_rect_fbb_b (@list_rect_fbb_b)
+      ; with_name ident_list_rect_fbb_b_b (@list_rect_fbb_b_b)
+      ; with_name ident_list_rect_fbb_b_b_b (@list_rect_fbb_b_b_b)
+      ; with_name ident_list_rect_fbb_b_b_b_b (@list_rect_fbb_b_b_b_b)
+      ; with_name ident_list_rect_fbb_b_b_b_b_b (@list_rect_fbb_b_b_b_b_b)
+*)
       ; with_name ident_list_case (@Thunked.list_case)
       ; with_name ident_List_length (@List.length)
       ; with_name ident_List_seq (@List.seq)
@@ -131,6 +143,8 @@ Definition all_ident_named_interped : InductiveHList.hlist
       ; with_name ident_List_update_nth (@update_nth)
       ; with_name ident_List_nth_default (@nth_default)
       ; with_name ident_eager_List_nth_default (ident.eagerly (@nth_default))
+      ; with_name ident_Pos_add Pos.add
+      ; with_name ident_Pos_mul Pos.mul
       ; with_name ident_Z_add Z.add
       ; with_name ident_Z_mul Z.mul
       ; with_name ident_Z_pow Z.pow
@@ -147,12 +161,15 @@ Definition all_ident_named_interped : InductiveHList.hlist
       ; with_name ident_Z_log2_up Z.log2_up
       ; with_name ident_Z_of_nat Z.of_nat
       ; with_name ident_Z_to_nat Z.to_nat
+      ; with_name ident_Z_pos Z.pos
+      ; with_name ident_Z_to_pos Z.to_pos
       ; with_name ident_Z_shiftr Z.shiftr
       ; with_name ident_Z_shiftl Z.shiftl
       ; with_name ident_Z_land Z.land
       ; with_name ident_Z_lor Z.lor
       ; with_name ident_Z_min Z.min
       ; with_name ident_Z_max Z.max
+      ; with_name ident_Z_abs Z.abs
       ; with_name ident_Z_mul_split Z.mul_split
       ; with_name ident_Z_mul_high Z.mul_high
       ; with_name ident_Z_add_get_carry Z.add_get_carry_full
diff --git a/src/Language/PreExtra.v b/src/Language/PreExtra.v
index 4bc9d22bdc..a06230d5d9 100644
--- a/src/Language/PreExtra.v
+++ b/src/Language/PreExtra.v
@@ -135,3 +135,75 @@ Module Thunked.
   Notation nat_rect := Rewriter.Util.NatUtil.Thunked.nat_rect (only parsing).
   Notation option_rect := Rewriter.Util.Option.Thunked.option_rect (only parsing).
 End Thunked.
+
+Definition nat_rect_fbb_b {A B C} :=
+  @Coq.Init.Datatypes.nat_rect (fun _ => (A -> B) -> C).
+Definition nat_rect_fbb_b_b {A B C D} :=
+  @Coq.Init.Datatypes.nat_rect (fun _ => (A -> B) -> C -> D).
+
+Definition list_rect_fbb_b {T A B C} :=
+  @Coq.Init.Datatypes.list_rect T (fun _ => (A -> B) -> C).
+Definition list_rect_fbb_b_b {T A B C D} :=
+  @Coq.Init.Datatypes.list_rect T (fun _ => (A -> B) -> C -> D).
+Definition list_rect_fbb_b_b_b {T A B C D E} :=
+  @Coq.Init.Datatypes.list_rect T (fun _ => (A -> B) -> C -> D -> E).
+Definition list_rect_fbb_b_b_b_b {T A B C D E F} :=
+  @Coq.Init.Datatypes.list_rect T (fun _ => (A -> B) -> C -> D -> E -> F).
+Definition list_rect_fbb_b_b_b_b_b {T A B C D E F G} :=
+  @Coq.Init.Datatypes.list_rect T (fun _ => (A -> B) -> C -> D -> E -> F -> G).
+
+Lemma unfold1_nat_rect_fbb_b {A B C} fO fS n k :
+  @nat_rect_fbb_b A B C fO fS n k =
+    if Nat.eqb 0 n then fO k else fS (pred n) (nat_rect_fbb_b fO fS (pred n)) k.
+Proof. case n; trivial. Qed.
+
+Lemma unfold1_nat_rect_fbb_b_b {A B C D} fO fS n k x :
+  @nat_rect_fbb_b_b A B C D fO fS n k x =
+    if Nat.eqb 0 n then fO k x else fS (pred n) (nat_rect_fbb_b_b fO fS (pred n)) k x.
+Proof. case n; trivial. Qed.
+
+Lemma unfold1_list_rect_fbb_b {T A B C} fnil fcons l k :
+  @list_rect_fbb_b T A B C fnil fcons l k =
+    match l with
+    | nil => fnil k
+    | cons x l => fcons x l (list_rect_fbb_b fnil fcons l) k
+    end.
+Proof. case l; trivial. Qed.
+
+Lemma unfold1_list_rect_fbb_b_b {T A B C D} fnil fcons l k c :
+  @list_rect_fbb_b_b T A B C D fnil fcons l k c =
+    match l with
+    | nil => fnil k c
+    | cons x l => fcons x l (list_rect_fbb_b_b fnil fcons l) k c
+    end.
+Proof. case l; trivial. Qed.
+
+Lemma unfold1_list_rect_fbb_b_b_b {T A B C D E} fnil fcons l k c d :
+  @list_rect_fbb_b_b_b T A B C D E fnil fcons l k c d =
+    match l with
+    | nil => fnil k c d
+    | cons x l => fcons x l (list_rect_fbb_b_b_b fnil fcons l) k c d
+    end.
+Proof. case l; trivial. Qed.
+
+Lemma unfold1_list_rect_fbb_b_b_b_b {T A B C D E F} fnil fcons l k c d e :
+  @list_rect_fbb_b_b_b_b T A B C D E F fnil fcons l k c d e =
+    match l with
+    | nil => fnil k c d e
+    | cons x l => fcons x l (list_rect_fbb_b_b_b_b fnil fcons l) k c d e
+    end.
+Proof. case l; trivial. Qed.
+
+Lemma unfold1_list_rect_fbb_b_b_b_b_b {T A B C D E F G} fnil fcons l k c d e f :
+  @list_rect_fbb_b_b_b_b_b T A B C D E F G fnil fcons l k c d e f =
+    match l with
+    | nil => fnil k c d e f
+    | cons x l => fcons x l (list_rect_fbb_b_b_b_b_b fnil fcons l) k c d e f
+    end.
+Proof. case l; trivial. Qed.
+
+Import Coq.Classes.Morphisms.
+
+Global Instance Proper_nat_rect_fbb_b {A B C} :
+  Proper (((eq ==> eq) ==> eq) ==> (eq ==> ((eq ==> eq) ==> eq) ==> (eq ==> eq) ==> eq) ==> eq ==> (eq ==> eq) ==> eq) (@nat_rect_fbb_b A B C) | 10.
+Proof. cbv -[nat_rect]; intros ??? ??? n m ?; subst m. induction n; cbn; eauto. Qed.
diff --git a/src/Stringification/IR.v b/src/Stringification/IR.v
index 3459964df1..abe9e67816 100644
--- a/src/Stringification/IR.v
+++ b/src/Stringification/IR.v
@@ -793,6 +793,8 @@ Module Compilers.
                  | ident.Nat_add
                  | ident.Nat_sub
                  | ident.Nat_eqb
+                 | ident.Pos_add
+                 | ident.Pos_mul
                  | ident.prod_rect _ _ _
                  | ident.bool_rect _
                  | ident.bool_rect_nodep _
@@ -807,6 +809,15 @@ Module Compilers.
                  | ident.eager_list_rect _ _
                  | ident.list_rect_arrow _ _ _
                  | ident.eager_list_rect_arrow _ _ _
+                 (*
+                 | ident.nat_rect_fbb_b _ _ _
+                 | ident.nat_rect_fbb_b_b _ _ _ _
+                 | ident.list_rect_fbb_b _ _ _ _
+                 | ident.list_rect_fbb_b_b _ _ _ _ _
+                 | ident.list_rect_fbb_b_b_b _ _ _ _ _ _
+                 | ident.list_rect_fbb_b_b_b_b _ _ _ _ _ _ _
+                 | ident.list_rect_fbb_b_b_b_b_b _ _ _ _ _ _ _ _
+                  *)
                  | ident.list_case _ _
                  | ident.List_length _
                  | ident.List_seq
@@ -834,10 +845,13 @@ Module Compilers.
                  | ident.Z_gtb
                  | ident.Z_min
                  | ident.Z_max
+                 | ident.Z_abs
                  | ident.Z_log2
                  | ident.Z_log2_up
                  | ident.Z_of_nat
                  | ident.Z_to_nat
+                 | ident.Z_pos
+                 | ident.Z_to_pos
                  | ident.Z_ltz
                  | ident.Z_zselect
                  | ident.Z_mul_split
diff --git a/src/Stringification/Language.v b/src/Stringification/Language.v
index 570a40e5f7..a7cca8915e 100644
--- a/src/Stringification/Language.v
+++ b/src/Stringification/Language.v
@@ -177,6 +177,7 @@ Module Compilers.
             := match t return ShowLevel (ZRange.type.base.interp t) with
                | base.type.unit => @show_lvl unit _
                | base.type.type_base base.type.Z => @show_lvl zrange _
+               | base.type.type_base base.type.positive => @show_lvl positive _
                | base.type.type_base base.type.bool => @show_lvl bool _
                | base.type.type_base base.type.nat => @show_lvl nat _
                | base.type.type_base base.type.zrange => @show_lvl zrange _
@@ -191,11 +192,7 @@ Module Compilers.
             Fixpoint show_lvl_interp {t} : ShowLevel (ZRange.type.base.option.interp t)
               := match t return ShowLevel (ZRange.type.base.option.interp t) with
                  | base.type.unit => @show_lvl unit _
-                 | base.type.type_base base.type.Z => @show_lvl (option zrange) _
-                 | base.type.type_base base.type.bool => @show_lvl (option bool) _
-                 | base.type.type_base base.type.nat => @show_lvl (option nat) _
-                 | base.type.type_base base.type.zrange => @show_lvl (option zrange) _
-                 | base.type.type_base base.type.string => @show_lvl (option string) _
+                 | base.type.type_base _ as t => @show_lvl (option (ZRange.type.base.interp t)) _
                  | base.type.prod A B => @show_lvl (ZRange.type.base.option.interp A * ZRange.type.base.option.interp B) _
                  | base.type.list A => @show_lvl (option (list (ZRange.type.base.option.interp A))) _
                  | base.type.option A => @show_lvl (option (option (ZRange.type.base.option.interp A))) _
@@ -222,6 +219,7 @@ Module Compilers.
           Global Instance show_base : Show base.type.base
             := fun t => match t with
                         | base.type.Z => "ℤ"
+                        | base.type.positive => "ℤ⁺"
                         | base.type.bool => "𝔹"
                         | base.type.nat => "ℕ"
                         | base.type.zrange => "zrange"
@@ -246,6 +244,7 @@ Module Compilers.
             := match t with
                | base.type.Z => @show_lvl Z _
                | base.type.bool => @show_lvl bool _
+               | base.type.positive => @show_lvl positive _
                | base.type.nat => @show_lvl nat _
                | base.type.zrange => @show_lvl zrange _
                | base.type.string => @show_lvl string _
@@ -398,6 +397,8 @@ Module Compilers.
                 | ident.Nat_add => neg_wrap_parens "Nat.add"
                 | ident.Nat_sub => neg_wrap_parens "Nat.sub"
                 | ident.Nat_eqb => neg_wrap_parens "Nat.eqb"
+                | ident.Pos_mul => neg_wrap_parens "Pos.mul"
+                | ident.Pos_add => neg_wrap_parens "Pos.add"
                 | ident.nil t => neg_wrap_parens "[]"
                 | ident.cons t => fun _ => "(::)"
                 | ident.pair A B => fun _ => "(,)"
@@ -410,6 +411,15 @@ Module Compilers.
                 | ident.eager_nat_rect P => neg_wrap_parens "eager_nat_rect"
                 | ident.nat_rect_arrow P Q => neg_wrap_parens "nat_rect(→)"
                 | ident.eager_nat_rect_arrow P Q => neg_wrap_parens "eager_nat_rect(→)"
+                (*
+                | @ident.nat_rect_fbb_b A B C => neg_wrap_parens "nat_rect_fbb_b"
+                | @ident.nat_rect_fbb_b_b A B C D => neg_wrap_parens "nat_rect_fbb_b_b"
+                | @ident.list_rect_fbb_b T A B C => neg_wrap_parens "list_rect_fbb_b"
+                | @ident.list_rect_fbb_b_b T A B C D => neg_wrap_parens "list_rect_fbb_b_b"
+                | @ident.list_rect_fbb_b_b_b T A B C D E => neg_wrap_parens "list_rect_fbb_b_b"
+                | @ident.list_rect_fbb_b_b_b_b T A B C D E F => neg_wrap_parens "list_rect_fbb_b_b"
+                | @ident.list_rect_fbb_b_b_b_b_b T A B C D E F G => neg_wrap_parens "list_rect_fbb_b_b"
+                 *)
                 | ident.list_rect A P => neg_wrap_parens "list_rect"
                 | ident.eager_list_rect A P => neg_wrap_parens "eager_list_rect"
                 | ident.list_rect_arrow A P Q => neg_wrap_parens "list_rect(→)"
@@ -448,10 +458,13 @@ Module Compilers.
                 | ident.Z_gtb => fun _ => "(>)"
                 | ident.Z_min => neg_wrap_parens "min"
                 | ident.Z_max => neg_wrap_parens "max"
+                | ident.Z_abs => neg_wrap_parens "abs"
                 | ident.Z_log2 => neg_wrap_parens "log₂"
                 | ident.Z_log2_up => neg_wrap_parens "⌈log₂⌉"
                 | ident.Z_of_nat => fun _ => "(ℕ→ℤ)"
                 | ident.Z_to_nat => fun _ => "(ℤ→ℕ)"
+                | ident.Z_pos => fun _ => "(ℤ⁺→ℤ)"
+                | ident.Z_to_pos => fun _ => "(ℤ→ℤ⁺)"
                 | ident.Z_shiftr => fun _ => "(>>)"
                 | ident.Z_shiftl => fun _ => "(<<)"
                 | ident.Z_land => fun _ => "(&)"
@@ -505,6 +518,8 @@ Module Compilers.
               ; ("+ℕ", (add_assoc, add_lvl))
               ; ("-ℕ", (sub_assoc, sub_lvl))
               ; ("=ℕ", (NoAssoc, Level.level 70))
+              ; ("*ℤ⁺", (mul_assoc, mul_lvl))
+              ; ("+ℤ⁺", (add_assoc, add_lvl))
               ; ("::", (RightAssoc, Level.level 60))
               ; ("++", (FullyAssoc, Level.level 60))
               ; ("*", (mul_assoc, mul_lvl))
@@ -575,6 +590,8 @@ Module Compilers.
              | ident.Nat_add => "+ℕ"
              | ident.Nat_sub => "-ℕ"
              | ident.Nat_eqb => "=ℕ"
+             | ident.Pos_mul => "*ℤ⁺"
+             | ident.Pos_add => "+ℤ⁺"
              | ident.cons _ => "::"
              | ident.List_app _ => "++"
              | ident.Z_mul => "*"
@@ -627,6 +644,8 @@ Module Compilers.
              | ident.Nat_add as idc
              | ident.Nat_sub as idc
              | ident.Nat_eqb as idc
+             | ident.Pos_mul as idc
+             | ident.Pos_add as idc
              | ident.cons _ as idc
              | ident.List_app _ as idc
              | ident.Z_mul as idc
@@ -687,6 +706,15 @@ Module Compilers.
              | ident.eager_nat_rect _ as idc
              | ident.eager_nat_rect_arrow _ _ as idc
              | ident.nat_rect_arrow _ _ as idc
+             (*
+             | @ident.nat_rect_fbb_b    _ _ _ as idc
+             | @ident.nat_rect_fbb_b_b  _ _ _ _ as idc
+             | @ident.list_rect_fbb_b   _ _ _ _ as idc
+             | @ident.list_rect_fbb_b_b _ _ _ _ _ as idc
+             | @ident.list_rect_fbb_b_b_b _ _ _ _ _ _ as idc
+             | @ident.list_rect_fbb_b_b_b_b _ _ _ _ _ _ _ as idc
+             | @ident.list_rect_fbb_b_b_b_b_b  _ _ _ _ _ _ _ _ as idc
+              *)
              | ident.option_rect _ _ as idc
              | ident.list_rect _ _ as idc
              | ident.eager_list_rect _ _ as idc
@@ -710,8 +738,11 @@ Module Compilers.
              | ident.Z_log2_up as idc
              | ident.Z_of_nat as idc
              | ident.Z_to_nat as idc
+             | ident.Z_pos as idc
+             | ident.Z_to_pos as idc
              | ident.Z_min as idc
              | ident.Z_max as idc
+             | ident.Z_abs as idc
              | ident.Z_mul_split as idc
              | ident.Z_mul_high as idc
              | ident.Z_add_get_carry as idc