diff --git a/theories/well_founded.v b/theories/well_founded.v
index 4a4a7003a1fe1174b27aac2d30615a747098350a..91a47fa7bcf622b78f6ad2656ca276e058dc7b6a 100644
--- a/theories/well_founded.v
+++ b/theories/well_founded.v
@@ -55,3 +55,14 @@ Proof.
   apply HF; intros.
   apply Fix_F_proper; auto.
 Qed.
+
+(**
+Generate an induction principle for [Acc] for reasoning about recursion on
+[Acc], such as [countable.choose_proper].
+
+We need an induction principle to prove predicates of [Acc] values, with
+conclusion [∀ (x : A) (a : Acc R x), P x a]. Instead, [Acc_ind] has conclusion
+[∀ x : A, Acc R x → P x], as if it were generated by
+[Scheme Acc_rect := Minimality for Acc Sort Prop.]
+*)
+Scheme Acc_dep_ind := Induction for Acc Sort Prop.