diff --git a/Util/ListComplements.v b/Util/ListComplements.v index ead544c0868c2c1743761bde2911034b6e472af2..2ab5efa5870ace40f7c40227b312022749905a28 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 .