Add list_rect_arrow

After     | File Name                                                   | Before    || Change    | % Change
-----------------------------------------------------------------------------------------------------------
36m06.27s | Total                                                       | 35m50.70s || +0m15.57s | +0.72%
-----------------------------------------------------------------------------------------------------------
2m45.00s  | Fancy/Compiler.vo                                           | 2m40.67s  || +0m04.32s | +2.69%
1m05.90s  | GENERATEDIdentifiersWithoutTypesProofs.vo                   | 1m02.06s  || +0m03.84s | +6.18%
0m19.29s  | PushButtonSynthesis/BarrettReductionReificationCache.vo     | 0m16.24s  || +0m03.05s | +18.78%
2m55.24s  | PushButtonSynthesis/WordByWordMontgomeryReificationCache.vo | 2m57.84s  || -0m02.59s | -1.46%
1m56.35s  | RewriterRulesGood.vo                                        | 1m54.16s  || +0m02.18s | +1.91%
0m41.32s  | ExtractionHaskell/unsaturated_solinas                       | 0m39.10s  || +0m02.21s | +5.67%
0m34.84s  | AbstractInterpretationProofs.vo                             | 0m32.77s  || +0m02.07s | +6.31%
0m17.77s  | p448_solinas_64.c                                           | 0m20.12s  || -0m02.35s | -11.67%
2m01.09s  | RewriterWf2.vo                                              | 1m59.61s  || +0m01.48s | +1.23%
1m48.15s  | RewriterRulesInterpGood.vo                                  | 1m49.56s  || -0m01.40s | -1.28%
1m21.56s  | Rewriter.vo                                                 | 1m22.98s  || -0m01.42s | -1.71%
0m57.30s  | ExtractionHaskell/word_by_word_montgomery                   | 0m58.76s  || -0m01.46s | -2.48%
0m47.94s  | p521_32.c                                                   | 0m46.84s  || +0m01.09s | +2.34%
0m38.63s  | Fancy/Montgomery256.vo                                      | 0m37.28s  || +0m01.35s | +3.62%
0m26.01s  | SlowPrimeSynthesisExamples.vo                               | 0m24.90s  || +0m01.11s | +4.45%
0m13.56s  | ExtractionOCaml/unsaturated_solinas                         | 0m12.32s  || +0m01.24s | +10.06%
0m09.90s  | ExtractionOCaml/unsaturated_solinas.ml                      | 0m08.70s  || +0m01.20s | +13.79%
3m16.06s  | p384_32.c                                                   | 3m15.80s  || +0m00.25s | +0.13%
1m46.10s  | Fancy/Barrett256.vo                                         | 1m47.02s  || -0m00.92s | -0.85%
0m56.15s  | RewriterInterpProofs1.vo                                    | 0m56.60s  || -0m00.45s | -0.79%
0m54.38s  | AbstractInterpretationWf.vo                                 | 0m53.72s  || +0m00.66s | +1.22%
0m44.40s  | PushButtonSynthesis/UnsaturatedSolinasReificationCache.vo   | 0m44.48s  || -0m00.07s | -0.17%
0m43.51s  | LanguageInversion.vo                                        | 0m42.77s  || +0m00.73s | +1.73%
0m41.61s  | UnderLetsProofs.vo                                          | 0m41.02s  || +0m00.58s | +1.43%
0m39.63s  | p521_64.c                                                   | 0m39.86s  || -0m00.22s | -0.57%
0m36.21s  | PushButtonSynthesis/UnsaturatedSolinas.vo                   | 0m36.25s  || -0m00.03s | -0.11%
0m32.80s  | AbstractInterpretationZRangeProofs.vo                       | 0m33.19s  || -0m00.39s | -1.17%
0m30.94s  | ExtractionHaskell/saturated_solinas                         | 0m30.24s  || +0m00.70s | +2.31%
0m29.79s  | PushButtonSynthesis/MontgomeryReductionReificationCache.vo  | 0m30.53s  || -0m00.74s | -2.42%
0m29.47s  | LanguageWf.vo                                               | 0m29.89s  || -0m00.42s | -1.40%
0m26.82s  | PushButtonSynthesis/WordByWordMontgomery.vo                 | 0m26.79s  || +0m00.03s | +0.11%
0m25.66s  | RewriterWf1.vo                                              | 0m25.60s  || +0m00.05s | +0.23%
0m22.53s  | ExtractionOCaml/word_by_word_montgomery                     | 0m22.10s  || +0m00.42s | +1.94%
0m19.93s  | secp256k1_32.c                                              | 0m19.65s  || +0m00.28s | +1.42%
0m19.36s  | p256_32.c                                                   | 0m19.96s  || -0m00.60s | -3.00%
0m16.44s  | CStringification.vo                                         | 0m16.20s  || +0m00.24s | +1.48%
0m16.13s  | p434_64.c                                                   | 0m15.73s  || +0m00.39s | +2.54%
0m13.93s  | ExtractionOCaml/word_by_word_montgomery.ml                  | 0m13.21s  || +0m00.71s | +5.45%
0m12.76s  | GENERATEDIdentifiersWithoutTypes.vo                         | 0m12.35s  || +0m00.41s | +3.31%
0m09.96s  | ExtractionOCaml/saturated_solinas                           | 0m10.05s  || -0m00.08s | -0.89%
0m09.08s  | p224_32.c                                                   | 0m08.38s  || +0m00.69s | +8.35%
0m08.38s  | ExtractionHaskell/word_by_word_montgomery.hs                | 0m08.55s  || -0m00.16s | -1.98%
0m07.65s  | p384_64.c                                                   | 0m08.54s  || -0m00.88s | -10.42%
0m06.72s  | ExtractionHaskell/unsaturated_solinas.hs                    | 0m06.69s  || +0m00.02s | +0.44%
0m06.64s  | BoundsPipeline.vo                                           | 0m06.58s  || +0m00.05s | +0.91%
0m06.58s  | PushButtonSynthesis/SaturatedSolinasReificationCache.vo     | 0m06.48s  || +0m00.09s | +1.54%
0m06.50s  | ExtractionOCaml/saturated_solinas.ml                        | 0m07.02s  || -0m00.51s | -7.40%
0m05.84s  | Fancy/Prod.vo                                               | 0m05.75s  || +0m00.08s | +1.56%
0m04.96s  | ExtractionHaskell/saturated_solinas.hs                      | 0m05.78s  || -0m00.82s | -14.18%
0m03.50s  | PushButtonSynthesis/Primitives.vo                           | 0m03.35s  || +0m00.14s | +4.47%
0m03.41s  | PushButtonSynthesis/SmallExamples.vo                        | 0m03.29s  || +0m00.12s | +3.64%
0m03.19s  | PushButtonSynthesis/BarrettReduction.vo                     | 0m03.26s  || -0m00.06s | -2.14%
0m03.18s  | curve25519_32.c                                             | 0m02.47s  || +0m00.71s | +28.74%
0m03.14s  | PushButtonSynthesis/SaturatedSolinas.vo                     | 0m03.25s  || -0m00.10s | -3.38%
0m02.86s  | PushButtonSynthesis/MontgomeryReduction.vo                  | 0m02.73s  || +0m00.12s | +4.76%
0m02.85s  | MiscCompilerPassesProofs.vo                                 | 0m03.76s  || -0m00.90s | -24.20%
0m02.15s  | curve25519_64.c                                             | 0m02.16s  || -0m00.01s | -0.46%
0m01.59s  | secp256k1_64.c                                              | 0m01.68s  || -0m00.08s | -5.35%
0m01.36s  | Language.vo                                                 | 0m01.25s  || +0m00.11s | +8.80%
0m01.35s  | CLI.vo                                                      | 0m01.35s  || +0m00.00s | +0.00%
0m01.29s  | p224_64.c                                                   | 0m01.59s  || -0m00.30s | -18.86%
0m01.29s  | p256_64.c                                                   | 0m01.33s  || -0m00.04s | -3.00%
0m01.25s  | CompilersTestCases.vo                                       | 0m01.55s  || -0m00.30s | -19.35%
0m01.22s  | AbstractInterpretation.vo                                   | 0m01.28s  || -0m00.06s | -4.68%
0m01.12s  | StandaloneHaskellMain.vo                                    | 0m01.14s  || -0m00.01s | -1.75%
0m01.12s  | StandaloneOCamlMain.vo                                      | 0m01.10s  || +0m00.02s | +1.81%
0m01.01s  | RewriterProofs.vo                                           | 0m01.14s  || -0m00.12s | -11.40%
0m00.74s  | MiscCompilerPasses.vo                                       | 0m00.68s  || +0m00.05s | +8.82%
0m00.70s  | PushButtonSynthesis/ReificationCache.vo                     | 0m00.50s  || +0m00.19s | +39.99%
0m00.69s  | PushButtonSynthesis/LegacySynthesisTactics.vo               | 0m00.64s  || +0m00.04s | +7.81%
0m00.49s  | UnderLets.vo                                                | 0m00.51s  || -0m00.02s | -3.92%

4 files changed, 62 insertions, 15 deletions

diff --git a/src/AbstractInterpretation.v b/src/AbstractInterpretation.v
index 808128025..ca0cb68bd 100644
--- a/src/AbstractInterpretation.v
+++ b/src/AbstractInterpretation.v
@@ -520,8 +520,8 @@ Module Compilers.
                          n
                    | None => ZRange.type.base.option.None
                    end
-             | ident.eager_nat_rect_arrow _ _
              | ident.nat_rect_arrow _ _
+             | ident.eager_nat_rect_arrow _ _
                => fun O_case S_case n v
                  => match n with
                    | Some n
@@ -533,8 +533,8 @@ Module Compilers.
                          v
                    | None => ZRange.type.base.option.None
                    end
-             | ident.eager_list_rect _ _
              | ident.list_rect _ _
+             | ident.eager_list_rect _ _
                => fun N C ls
                  => match ls with
                    | Some ls
@@ -545,6 +545,7 @@ 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
diff --git a/src/CStringification.v b/src/CStringification.v
index 3560a5f82..ff455130b 100644
--- a/src/CStringification.v
+++ b/src/CStringification.v
@@ -253,6 +253,8 @@ Module Compilers.
                => fun args => (show_application with_casts (fun _ => "list_rect") args, ZRange.type.base.option.None)
              | ident.eager_list_rect A P
                => fun args => (show_application with_casts (fun _ => "eager_list_rect") args, ZRange.type.base.option.None)
+             | ident.list_rect_arrow A P Q
+               => fun args => (show_application with_casts (fun _ => "list_rect(→)") args, ZRange.type.base.option.None)
              | ident.eager_list_rect_arrow A P Q
                => fun args => (show_application with_casts (fun _ => "eager_list_rect(→)") args, ZRange.type.base.option.None)
              | ident.list_case A P
@@ -394,6 +396,7 @@ Module Compilers.
                 | ident.eager_nat_rect_arrow P Q => "eager_nat_rect(→)"
                 | ident.list_rect A P => "list_rect"
                 | ident.eager_list_rect A P => "eager_list_rect"
+                | ident.list_rect_arrow A P Q => "list_rect(→)"
                 | ident.eager_list_rect_arrow A P Q => "eager_list_rect(→)"
                 | ident.list_case A P => "list_case"
                 | ident.List_length T => "length"
@@ -1300,6 +1303,7 @@ Module Compilers.
                | ident.option_rect _ _
                | ident.list_rect _ _
                | ident.eager_list_rect _ _
+               | ident.list_rect_arrow _ _ _
                | ident.eager_list_rect_arrow _ _ _
                | ident.list_case _ _
                | ident.List_length _
diff --git a/src/GENERATEDIdentifiersWithoutTypes.v b/src/GENERATEDIdentifiersWithoutTypes.v
index c250253e1..db84a33a3 100644
--- a/src/GENERATEDIdentifiersWithoutTypes.v
+++ b/src/GENERATEDIdentifiersWithoutTypes.v
@@ -276,6 +276,21 @@ print_ident = r"""Inductive ident : defaults.type -> Set :=
                    (fun x : Compilers.base.type => type.base x)
                      (Compilers.base.type.list A) ->
                    (fun x : Compilers.base.type => type.base x) P)%ptype
+  | list_rect_arrow : forall A P Q : Compilers.base.type,
+                      ident
+                        (((fun x : Compilers.base.type => type.base x) P ->
+                          (fun x : Compilers.base.type => type.base x) Q) ->
+                         ((fun x : Compilers.base.type => type.base x) A ->
+                          (fun x : Compilers.base.type => type.base x)
+                            (Compilers.base.type.list A) ->
+                          ((fun x : Compilers.base.type => type.base x) P ->
+                           (fun x : Compilers.base.type => type.base x) Q) ->
+                          (fun x : Compilers.base.type => type.base x) P ->
+                          (fun x : Compilers.base.type => type.base x) Q) ->
+                         (fun x : Compilers.base.type => type.base x)
+                           (Compilers.base.type.list A) ->
+                         (fun x : Compilers.base.type => type.base x) P ->
+                         (fun x : Compilers.base.type => type.base x) Q)%ptype
   | eager_list_rect : forall A P : Compilers.base.type,
                       ident
                         (((fun x : Compilers.base.type => type.base x)
@@ -865,6 +880,7 @@ show_match_ident = r"""match # with
  | ident.eager_nat_rect P =>
  | ident.eager_nat_rect_arrow P Q =>
  | ident.list_rect A P =>
+ | ident.list_rect_arrow A P Q =>
  | ident.eager_list_rect A P =>
  | ident.eager_list_rect_arrow A P Q =>
  | ident.list_case A P =>
@@ -1475,6 +1491,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
         | eager_nat_rect
         | eager_nat_rect_arrow
         | list_rect
+        | list_rect_arrow
         | eager_list_rect
         | eager_list_rect_arrow
         | list_case
@@ -1569,6 +1586,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | eager_nat_rect => Compilers.base.type
              | eager_nat_rect_arrow => Compilers.base.type * Compilers.base.type
              | list_rect => Compilers.base.type * Compilers.base.type
+             | list_rect_arrow => Compilers.base.type * Compilers.base.type * Compilers.base.type
              | eager_list_rect => Compilers.base.type * Compilers.base.type
              | eager_list_rect_arrow => Compilers.base.type * Compilers.base.type * Compilers.base.type
              | list_case => Compilers.base.type * Compilers.base.type
@@ -1664,6 +1682,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | eager_nat_rect => false
              | eager_nat_rect_arrow => false
              | list_rect => false
+             | list_rect_arrow => false
              | eager_list_rect => false
              | eager_list_rect_arrow => false
              | list_case => false
@@ -1759,6 +1778,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | eager_nat_rect, Compilers.ident.eager_nat_rect P => Datatypes.Some P
              | eager_nat_rect_arrow, Compilers.ident.eager_nat_rect_arrow P Q => Datatypes.Some (P, Q)
              | list_rect, Compilers.ident.list_rect A P => Datatypes.Some (A, P)
+             | list_rect_arrow, Compilers.ident.list_rect_arrow A P Q => Datatypes.Some (A, P, Q)
              | eager_list_rect, Compilers.ident.eager_list_rect A P => Datatypes.Some (A, P)
              | eager_list_rect_arrow, Compilers.ident.eager_list_rect_arrow A P Q => Datatypes.Some (A, P, Q)
              | list_case, Compilers.ident.list_case A P => Datatypes.Some (A, P)
@@ -1850,6 +1870,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | eager_nat_rect, _
              | eager_nat_rect_arrow, _
              | list_rect, _
+             | list_rect_arrow, _
              | eager_list_rect, _
              | eager_list_rect_arrow, _
              | list_case, _
@@ -1946,6 +1967,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | eager_nat_rect => fun P => ((type.base ()%etype -> type.base P) -> (type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P)%ptype
              | eager_nat_rect_arrow => fun arg => let '(P, Q) := eta2 arg in ((type.base P -> type.base Q) -> (type.base (Compilers.base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype
              | list_rect => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype
+             | list_rect_arrow => fun arg => let '(A, P, Q) := eta3 arg in ((type.base P -> type.base Q) -> (type.base A -> type.base (Compilers.base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.list A) -> type.base P -> type.base Q)%ptype
              | eager_list_rect => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype
              | eager_list_rect_arrow => fun arg => let '(A, P, Q) := eta3 arg in ((type.base P -> type.base Q) -> (type.base A -> type.base (Compilers.base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (Compilers.base.type.list A) -> type.base P -> type.base Q)%ptype
              | list_case => fun arg => let '(A, P) := eta2 arg in ((type.base ()%etype -> type.base P) -> (type.base A -> type.base (Compilers.base.type.list A) -> type.base P) -> type.base (Compilers.base.type.list A) -> type.base P)%ptype
@@ -2041,6 +2063,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
              | eager_nat_rect => fun P => @Compilers.ident.eager_nat_rect P
              | eager_nat_rect_arrow => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of eager_nat_rect_arrow arg') with (P, Q) => @Compilers.ident.eager_nat_rect_arrow P Q end
              | list_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of list_rect arg') with (A, P) => @Compilers.ident.list_rect A P end
+             | list_rect_arrow => fun arg => match eta3 arg as arg' return Compilers.ident.ident (type_of list_rect_arrow arg') with (A, P, Q) => @Compilers.ident.list_rect_arrow A P Q end
              | eager_list_rect => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of eager_list_rect arg') with (A, P) => @Compilers.ident.eager_list_rect A P end
              | eager_list_rect_arrow => fun arg => match eta3 arg as arg' return Compilers.ident.ident (type_of eager_list_rect_arrow arg') with (A, P, Q) => @Compilers.ident.eager_list_rect_arrow A P Q end
              | list_case => fun arg => match eta2 arg as arg' return Compilers.ident.ident (type_of list_case arg') with (A, P) => @Compilers.ident.list_case A P end
@@ -2143,6 +2166,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.eager_nat_rect P => f _ (@Compilers.ident.eager_nat_rect P)
            | Compilers.ident.eager_nat_rect_arrow P Q => f _ (@Compilers.ident.eager_nat_rect_arrow P Q)
            | Compilers.ident.list_rect A P => f _ (@Compilers.ident.list_rect A P)
+           | Compilers.ident.list_rect_arrow A P Q => f _ (@Compilers.ident.list_rect_arrow A P Q)
            | Compilers.ident.eager_list_rect A P => f _ (@Compilers.ident.eager_list_rect A P)
            | Compilers.ident.eager_list_rect_arrow A P Q => f _ (@Compilers.ident.eager_list_rect_arrow A P Q)
            | Compilers.ident.list_case A P => f _ (@Compilers.ident.list_case A P)
@@ -2237,6 +2261,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
       | eager_nat_rect {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base (base.type.type_base base.type.nat) -> type.base P -> type.base P) -> type.base (base.type.type_base base.type.nat) -> type.base P)%ptype
       | eager_nat_rect_arrow {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base (base.type.type_base base.type.nat) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.type_base base.type.nat) -> type.base P -> type.base Q)%ptype
       | list_rect {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype
+      | list_rect_arrow {A : base.type} {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base A -> type.base (base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.list A) -> type.base P -> type.base Q)%ptype
       | eager_list_rect {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype
       | eager_list_rect_arrow {A : base.type} {P : base.type} {Q : base.type} : ident ((type.base P -> type.base Q) -> (type.base A -> type.base (base.type.list A) -> (type.base P -> type.base Q) -> type.base P -> type.base Q) -> type.base (base.type.list A) -> type.base P -> type.base Q)%ptype
       | list_case {A : base.type} {P : base.type} : ident ((type.base ()%pbtype -> type.base P) -> (type.base A -> type.base (base.type.list A) -> type.base P) -> type.base (base.type.list A) -> type.base P)%ptype
@@ -2331,6 +2356,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @eager_nat_rect P => Raw.ident.eager_nat_rect
            | @eager_nat_rect_arrow P Q => Raw.ident.eager_nat_rect_arrow
            | @list_rect A P => Raw.ident.list_rect
+           | @list_rect_arrow A P Q => Raw.ident.list_rect_arrow
            | @eager_list_rect A P => Raw.ident.eager_list_rect
            | @eager_list_rect_arrow A P Q => Raw.ident.eager_list_rect_arrow
            | @list_case A P => Raw.ident.list_case
@@ -2426,6 +2452,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @eager_nat_rect P => []
            | @eager_nat_rect_arrow P Q => []
            | @list_rect A P => []
+           | @list_rect_arrow A P Q => []
            | @eager_list_rect A P => []
            | @eager_list_rect_arrow A P Q => []
            | @list_case A P => []
@@ -2521,6 +2548,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @eager_nat_rect P => fun _ => @Compilers.ident.eager_nat_rect _
            | @eager_nat_rect_arrow P Q => fun _ => @Compilers.ident.eager_nat_rect_arrow _ _
            | @list_rect A P => fun _ => @Compilers.ident.list_rect _ _
+           | @list_rect_arrow A P Q => fun _ => @Compilers.ident.list_rect_arrow _ _ _
            | @eager_list_rect A P => fun _ => @Compilers.ident.eager_list_rect _ _
            | @eager_list_rect_arrow A P Q => fun _ => @Compilers.ident.eager_list_rect_arrow _ _ _
            | @list_case A P => fun _ => @Compilers.ident.list_case _ _
@@ -2620,6 +2648,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @eager_nat_rect P, Compilers.ident.eager_nat_rect P' => Datatypes.Some tt
            | @eager_nat_rect_arrow P Q, Compilers.ident.eager_nat_rect_arrow P' Q' => Datatypes.Some tt
            | @list_rect A P, Compilers.ident.list_rect A' P' => Datatypes.Some tt
+           | @list_rect_arrow A P Q, Compilers.ident.list_rect_arrow A' P' Q' => Datatypes.Some tt
            | @eager_list_rect A P, Compilers.ident.eager_list_rect A' P' => Datatypes.Some tt
            | @eager_list_rect_arrow A P Q, Compilers.ident.eager_list_rect_arrow A' P' Q' => Datatypes.Some tt
            | @list_case A P, Compilers.ident.list_case A' P' => Datatypes.Some tt
@@ -2711,6 +2740,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | @eager_nat_rect _, _
            | @eager_nat_rect_arrow _ _, _
            | @list_rect _ _, _
+           | @list_rect_arrow _ _ _, _
            | @eager_list_rect _ _, _
            | @eager_list_rect_arrow _ _ _, _
            | @list_case _ _, _
@@ -2807,6 +2837,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.eager_nat_rect P => @eager_nat_rect (base.relax P)
            | Compilers.ident.eager_nat_rect_arrow P Q => @eager_nat_rect_arrow (base.relax P) (base.relax Q)
            | Compilers.ident.list_rect A P => @list_rect (base.relax A) (base.relax P)
+           | Compilers.ident.list_rect_arrow A P Q => @list_rect_arrow (base.relax A) (base.relax P) (base.relax Q)
            | Compilers.ident.eager_list_rect A P => @eager_list_rect (base.relax A) (base.relax P)
            | Compilers.ident.eager_list_rect_arrow A P Q => @eager_list_rect_arrow (base.relax A) (base.relax P) (base.relax Q)
            | Compilers.ident.list_case A P => @list_case (base.relax A) (base.relax P)
@@ -2902,6 +2933,7 @@ with open('GENERATEDIdentifiersWithoutTypes.v', 'w') as f:
            | Compilers.ident.eager_nat_rect P => tt
            | Compilers.ident.eager_nat_rect_arrow P Q => tt
            | Compilers.ident.list_rect A P => tt
+           | Compilers.ident.list_rect_arrow A P Q => tt
            | Compilers.ident.eager_list_rect A P => tt
            | Compilers.ident.eager_list_rect_arrow A P Q => tt
            | Compilers.ident.list_case A P => tt
diff --git a/src/Language.v b/src/Language.v
index 695073248..74c34b2f2 100644
--- a/src/Language.v
+++ b/src/Language.v
@@ -880,6 +880,7 @@ Module Compilers.
         | eager_nat_rect {P:base.type} : ident ((unit -> P) -> (nat -> P -> P) -> nat -> P)
         | eager_nat_rect_arrow {P Q:base.type} : ident ((P -> Q) -> (nat -> (P -> Q) -> (P -> Q)) -> nat -> P -> Q)
         | list_rect {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P -> P) -> list A -> P)
+        | list_rect_arrow {A P Q:base.type} : ident ((P -> Q) -> (A -> list A -> (P -> Q) -> (P -> Q)) -> list A -> P -> Q)
         | eager_list_rect {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P -> P) -> list A -> P)
         | eager_list_rect_arrow {A P Q:base.type} : ident ((P -> Q) -> (A -> list A -> (P -> Q) -> (P -> Q)) -> list A -> P -> Q)
         | list_case {A P:base.type} : ident ((unit -> P) -> (A -> list A -> P) -> list A -> P)
@@ -1058,17 +1059,15 @@ Module Compilers.
              | bool_rect T
                => fun t f => Datatypes.bool_rect _ (t tt) (f tt)
              | nat_rect P
-               => fun O_case S_case => Datatypes.nat_rect _ (O_case tt) S_case
-             | nat_rect_arrow P Q
-               => fun O_case S_case => Datatypes.nat_rect _ O_case S_case
              | eager_nat_rect P
                => fun O_case S_case => Datatypes.nat_rect _ (O_case tt) S_case
+             | nat_rect_arrow P Q
              | eager_nat_rect_arrow P Q
                => fun O_case S_case => Datatypes.nat_rect _ O_case S_case
              | list_rect A P
-               => fun N_case C_case => Datatypes.list_rect _ (N_case tt) C_case
              | eager_list_rect A P
                => fun N_case C_case => Datatypes.list_rect _ (N_case tt) C_case
+             | list_rect_arrow A P Q
              | eager_list_rect_arrow A P Q
                => fun N_case C_case => Datatypes.list_rect _ N_case C_case
              | list_case A P
@@ -1294,13 +1293,13 @@ Module Compilers.
              end
         | @Datatypes.nat_rect ?T0
           => lazymatch (eval cbv beta in T0) with
-            | (fun _ => ?P -> ?Q)
-              => let rP := base.reify P in
-                let rQ := base.reify Q in
-                then_tac (@ident.nat_rect_arrow rP rQ)
+             | (fun _ => ?P -> ?Q)
+               => let rP := base.reify P in
+                  let rQ := base.reify Q in
+                  then_tac (@ident.nat_rect_arrow rP rQ)
              | T0 => else_tac ()
              | ?T' => reify_rec (@Datatypes.nat_rect T')
-            end
+             end
         | @Thunked.nat_rect ?T
           => let rT := base.reify T in
              then_tac (@ident.nat_rect rT)
@@ -1325,10 +1324,21 @@ Module Compilers.
              then_tac (@ident.eager_nat_rect rT)
         | @Datatypes.list_rect ?A ?T0 ?Pnil
           => lazymatch (eval cbv beta in T0) with
-            | fun _ => ?T => reify_rec (@Thunked.list_rect A T (fun _ : Datatypes.unit => Pnil))
-            | T0 => else_tac ()
-            | ?T' => reify_rec (@Datatypes.list_rect A T' Pnil)
-            end
+             | fun _ => _ -> _ => else_tac ()
+             | fun _ => ?T => reify_rec (@Thunked.list_rect A T (fun _ : Datatypes.unit => Pnil))
+             | T0 => else_tac ()
+             | ?T' => reify_rec (@Datatypes.list_rect A T' Pnil)
+             end
+        | @Datatypes.list_rect ?A ?T0
+          => lazymatch (eval cbv beta in T0) with
+             | (fun _ => ?P -> ?Q)
+               => let rA := base.reify A in
+                  let rP := base.reify P in
+                  let rQ := base.reify Q in
+                  then_tac (@ident.list_rect_arrow rA rP rQ)
+             | T0 => else_tac ()
+             | ?T' => reify_rec (@Datatypes.list_rect A T')
+             end
         | @Thunked.list_rect ?A ?T
           => let rA := base.reify A in
              let rT := base.reify T in