From 37796369c7ff47a500d7d94602b57b71492ce3b1 Mon Sep 17 00:00:00 2001
From: Jason Gross <jgross@mit.edu>
Date: Tue, 6 Dec 2022 19:15:19 -0500
Subject: [PATCH] Add `hd_error_skipn_iff_In`

---
 template-coq/theories/utils/MCList.v | 14 ++++++++++++++
 1 file changed, 14 insertions(+)

diff --git a/template-coq/theories/utils/MCList.v b/template-coq/theories/utils/MCList.v
index 39d723ff0..3f2d0b92b 100644
--- a/template-coq/theories/utils/MCList.v
+++ b/template-coq/theories/utils/MCList.v
@@ -1454,3 +1454,17 @@ Proof.
   case=> [|l' z];
   [exact: (snoc_view_snoc nil) | exact: (snoc_view_snoc (a :: l'))].
 Qed.
+
+Lemma hd_error_skipn_iff_In {A v ls}
+  : (exists n, hd_error (@skipn A n ls) = Some v) <-> In v ls.
+Proof.
+  move: ls; elim => //=.
+  1: setoid_rewrite skipn_nil; cbn; firstorder congruence.
+  move => ?? <-.
+  split.
+  { move => [[|?]]; rewrite ?skipn_0 ?skipn_S => //=.
+    1: move => [->].
+    all: eauto. }
+  { move => [->|[n H]]; [ exists 0 | exists (S n) ];
+            rewrite ?skipn_0 ?skipn_S => //=. }
+Qed.