diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index a4b54719b1069e0c9cdfd456d3e2433a2e851d0c..f77d85ab5b1bc81b2693b1a452af6f81ddc3e2ec 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -93,7 +93,18 @@ Qed.
 Lemma ident_beq_reflect i1 i2 : reflect (i1 = i2) (ident_beq i1 i2).
 Proof. apply iff_reflect. by rewrite ident_beq_true. Qed.
 
-(** Copies of some [option] combinators for better reduction control. *)
+(** Copies of some [list] and [option] combinators for better reduction control. *)
+Definition pm_app {A} : list A → list A → list A :=
+  fix go l l' :=
+  match l with  [] => l' | x :: l => x :: go l l' end.
+Definition pm_rev_append {A} : list A → list A → list A :=
+  fix go l l' :=
+  match l with [] => l' | x :: l => go l (x :: l') end.
+Definition pm_reverse {A} (l : list A) : list A := pm_rev_append l [].
+Definition pm_foldr {A B} (f : B → A → A) (a : A) : list B → A :=
+  fix go l :=
+  match l with [] => a | x :: l => f x (go l) end.
+
 Definition pm_option_bind {A B} (f : A → option B) (mx : option A) : option B :=
   match mx with Some x => f x | None => None end.
 Arguments pm_option_bind {_ _} _ !_ /.
diff --git a/theories/proofmode/reduction.v b/theories/proofmode/reduction.v
index 690e6866e5bce7145750a8ba82acac4a3ec86cf9..2fece86719199e8802a8115f96fe9f4e9abb9953 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -14,7 +14,8 @@ Declare Reduction pm_eval := cbv [
   envs_simple_replace envs_replace envs_split
   envs_clear_spatial envs_clear_intuitionistic envs_set_counter envs_incr_counter
   envs_split_go envs_split env_to_prop
-  (* PM option combinators *)
+  (* PM list and option combinators *)
+  pm_app pm_rev_append pm_reverse pm_foldr
   pm_option_bind pm_from_option pm_option_fun
 ].
 Ltac pm_eval t :=