diff --git a/src/Rewriter/Rules.v b/src/Rewriter/Rules.v
index 61cf959fcf..08d5720641 100644
--- a/src/Rewriter/Rules.v
+++ b/src/Rewriter/Rules.v
@@ -183,6 +183,13 @@ Definition nbe_rewrite_rulesT : list (bool * Prop)
                             end)
                         ('n)
                         xs)
+              ; typeof! @unfold1_nat_rect_fbb_b
+              ; typeof! @unfold1_nat_rect_fbb_b_b
+              ; typeof! @unfold1_list_rect_fbb_b
+              ; typeof! @unfold1_list_rect_fbb_b_b
+              ; typeof! @unfold1_list_rect_fbb_b_b_b
+              ; typeof! @unfold1_list_rect_fbb_b_b_b_b
+              ; typeof! @unfold1_list_rect_fbb_b_b_b_b_b
              ]
         ].
 
diff --git a/src/Rewriter/RulesProofs.v b/src/Rewriter/RulesProofs.v
index 1eb8f63004..a4cac6b2b8 100644
--- a/src/Rewriter/RulesProofs.v
+++ b/src/Rewriter/RulesProofs.v
@@ -90,6 +90,13 @@ Local Hint Resolve
       eq_firstn_nat_rect
       eq_skipn_nat_rect
       eq_update_nth_nat_rect
+      unfold1_nat_rect_fbb_b
+      unfold1_nat_rect_fbb_b_b
+      unfold1_list_rect_fbb_b
+      unfold1_list_rect_fbb_b_b
+      unfold1_list_rect_fbb_b_b_b
+      unfold1_list_rect_fbb_b_b_b_b
+      unfold1_list_rect_fbb_b_b_b_b_b
   : core.
 
 (* to catch [prod_rect] and not just [prod_rect_nodep] *)