From 4a3e8ed01b8e48edc4e9cd2e61b7a8f674601968 Mon Sep 17 00:00:00 2001
From: Robbert Krebbers <mail@robbertkrebbers.nl>
Date: Tue, 12 Apr 2022 07:48:49 +0200
Subject: [PATCH] Add induction principle for `tele_arg`.

---
 theories/telescopes.v | 10 ++++++++++
 1 file changed, 10 insertions(+)

diff --git a/theories/telescopes.v b/theories/telescopes.v
index b44ecc82..3dad07ed 100644
--- a/theories/telescopes.v
+++ b/theories/telescopes.v
@@ -56,6 +56,16 @@ Notation TargO := tt (only parsing).
 Notation TargS a b := (@TeleArgCons _ (λ x, tele_arg _) a b) (only parsing).
 Coercion tele_arg : tele >-> Sortclass.
 
+Lemma tele_arg_ind (P : ∀ TT, tele_arg TT → Prop) :
+  P TeleO TargO →
+  (∀ T (b : T → tele) x xs, P (b x) xs → P (TeleS b) (TargS x xs)) →
+  ∀ TT (xs : tele_arg TT), P TT xs.
+Proof.
+  intros H0 HS TT. induction TT as [|T b IH]; simpl.
+  - by intros [].
+  - intros [x xs]. by apply HS.
+Qed.
+
 Fixpoint tele_app {TT : tele} {U} : (TT -t> U) -> TT → U :=
   match TT as TT return (TT -t> U) -> TT → U with
   | TeleO => λ F _, F
-- 
GitLab