From 8558f314f1f7407017dc175cf79ead887e68be2f Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?S=C3=A9bastien=20Bouchard?= <sebastien.bouchard@lip6.fr>
Date: Thu, 6 Jun 2024 12:46:43 +0200
Subject: [PATCH] Removal of useless lemma introduced in previous commit

---
 Util/ListComplements.v | 7 -------
 1 file changed, 7 deletions(-)

diff --git a/Util/ListComplements.v b/Util/ListComplements.v
index ead544c0..2ab5efa5 100644
--- a/Util/ListComplements.v
+++ b/Util/ListComplements.v
@@ -52,13 +52,6 @@ intros x l Hin. induction l.
 - destruct Hin. subst. now left. right. auto.
 Qed. *)
 
-Lemma hd_proof : forall l : list A, 0 < length l -> A.
-Proof using .
-  intros * H. destruct l as [|a t]. 2: exact a. exfalso.
-  rewrite (proj2 (length_zero_iff_nil _)) in H by reflexivity.
-  inversion H.
-Qed.
-
 Lemma all_eq : forall (l : list A) (a1 : A), In a1 l ->length l = 1
   -> forall a2 : A, In a2 l -> a2 = a1.
 Proof using .
-- 
GitLab