well_founded.v: add Acc_dep_ind induction principle for Acc

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.