From 2df65b35043a113f16f5af0116bc68dbc76a3c05 Mon Sep 17 00:00:00 2001
From: "Paolo G. Giarrusso" <p.giarrusso@gmail.com>
Date: Fri, 1 Oct 2021 20:17:22 +0200
Subject: [PATCH] well_founded.v: add Acc_dep_ind induction principle for Acc

---
 theories/well_founded.v | 11 +++++++++++
 1 file changed, 11 insertions(+)

diff --git a/theories/well_founded.v b/theories/well_founded.v
index 4a4a7003..91a47fa7 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.
-- 
GitLab