diff --git a/theories/proofmode/base.v b/theories/proofmode/base.v
index bc251fe259fe002c0f858b212c1763e98a433cd0..e50c8c88d01afe04a894150f55358621b3b51f45 100644
--- a/theories/proofmode/base.v
+++ b/theories/proofmode/base.v
@@ -98,7 +98,10 @@ 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 functions on [list] and [option] for better reduction control. *)
+Fixpoint pm_app {A} (l1 l2 : list A) : list A :=
+  match l1 with [] => l2 | x :: l1 => x :: pm_app l1 l2 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 0cfc076234865e9458a0f42fd5328dd36fb20e9e..6ce3ffd9c6f798cb1d1daad4be072d3afa1fb945 100644
--- a/theories/proofmode/reduction.v
+++ b/theories/proofmode/reduction.v
@@ -16,8 +16,8 @@ Declare Reduction pm_eval := cbv [
   envs_clear_spatial envs_clear_intuitionistic envs_incr_counter
   envs_split_go envs_split
   env_to_prop_go env_to_prop env_to_prop_and_go env_to_prop_and
-  (* PM option combinators *)
-  pm_option_bind pm_from_option pm_option_fun
+  (* PM list and option functions *)
+  pm_app pm_option_bind pm_from_option pm_option_fun
 ].
 Ltac pm_eval t :=
   eval pm_eval in t.