diff --git a/prelude/list.v b/prelude/list.v
index 42a40dc3c934e79a628aded52694c5a6ba8e6c8f..59b26331813bf82dc7cd243e88f8721e7b9fd82e 100644
--- a/prelude/list.v
+++ b/prelude/list.v
@@ -1265,6 +1265,21 @@ Proof.
     take_app_alt by (rewrite ?app_length, ?take_length, ?Hk; lia).
 Qed.
 
+(** ** Properties of the [imap] function *)
+Lemma imap_cons {B} (f : nat → A → B) x l :
+  imap f (x :: l) = f 0 x :: imap (f ∘ S) l.
+Proof.
+  unfold imap. simpl. f_equal. generalize 0.
+  induction l; intros n; simpl; repeat (auto||f_equal).
+Qed.
+Lemma imap_ext {B} (f g : nat → A → B) l :
+  (∀ i x, f i x = g i x) →
+  imap f l = imap g l.
+Proof.
+  unfold imap. intro EQ. generalize 0.
+  induction l; simpl; intros n; f_equal; auto.
+Qed.
+
 (** ** Properties of the [mask] function *)
 Lemma mask_nil f βs : mask f βs (@nil A) = [].
 Proof. by destruct βs. Qed.